Feat: implement verify_rust_std diff --hash-json and add snapshot tests in compare.rs

src/bin/verify_rust_std/diff.rs

@@ -1,7 +1,10 @@
 use crate::{Result, read_json};
 use clap::Parser;
-use distributed_verification::diff::{MergeHashKaniList, diff};
-use distributed_verification::logger;
+use distributed_verification::{
+    SerFunction,
+    diff::{MergeHashKaniList, diff_on_hashed_func, diff_on_merged},
+    logger,
+};
 
 pub fn run(args: &[String]) -> Result<()> {
     logger::init();
@@ -18,14 +21,33 @@ struct SubCmdDiff {
     /// Path to a recent merge.json that is generated by `verify_rust_std merge`.
     #[arg(long)]
     new: String,
+
+    /// Diff on hash.json which is directly produced by distributed-verification,
+    /// instead of merged.json which is produced by dv's merge subcmd.
+    #[arg(long, default_value_t)]
+    hash_json: bool,
 }
 
 impl SubCmdDiff {
     fn run(self) -> Result<()> {
+        if self.hash_json { self.diff_on_hashed_func() } else { self.diff_on_merge() }
+    }
+
+    fn diff_on_hashed_func(self) -> Result<()> {
+        let old: Vec<SerFunction> = read_json(&self.old)?;
+        let new: Vec<SerFunction> = read_json(&self.new)?;
+
+        let difference = diff_on_hashed_func(&old, &new);
+        serde_json::to_writer_pretty(std::io::stdout(), &difference)?;
+
+        Ok(())
+    }
+
+    fn diff_on_merge(self) -> Result<()> {
         let old: Vec<MergeHashKaniList> = read_json(&self.old)?;
         let new: Vec<MergeHashKaniList> = read_json(&self.new)?;
 
-        let difference = diff(&old, &new);
+        let difference = diff_on_merged(&old, &new);
         serde_json::to_writer_pretty(std::io::stdout(), &difference)?;
 
         Ok(())

src/diff.rs

@@ -267,7 +267,16 @@ pub struct MergeHashKaniList {
 ///
 /// If new is sorted, especially directly from the stdout of verify_rust_std merge subcommand,
 /// the result is sorted.
-pub fn diff(old: &[MergeHashKaniList], new: &[MergeHashKaniList]) -> Vec<MergeHashKaniList> {
+pub fn diff_on_merged(
+    old: &[MergeHashKaniList],
+    new: &[MergeHashKaniList],
+) -> Vec<MergeHashKaniList> {
     let set: HashSet<_> = old.iter().collect();
     new.iter().filter(|item| item.hash.is_none() || !set.contains(item)).cloned().collect()
 }
+
+/// Compare two hash.json.
+pub fn diff_on_hashed_func(old: &[SerFunction], new: &[SerFunction]) -> Vec<SerFunction> {
+    let set: HashSet<_> = old.iter().collect();
+    new.iter().filter(|item| !set.contains(item)).cloned().collect()
+}

src/lib.rs

@@ -123,7 +123,7 @@ pub fn kani_path() -> String {
     path
 }
 
-#[derive(Debug, Default, Serialize, Deserialize, Clone)]
+#[derive(Debug, Default, Hash, PartialEq, Eq, Serialize, Deserialize, Clone)]
 pub struct SerFunction {
     pub hash: Box<str>,
     pub name: Box<str>,

tests/compare.rs

@@ -1,5 +1,4 @@
-use std::fs::{copy, remove_file};
-
+use std::fs::{copy, create_dir_all, remove_file};
 mod utils;
 use utils::{assert_eq, *};
 
@@ -10,22 +9,38 @@ fn get(text: &str, start: &str) -> SerFunction {
 }
 
 const COMPARE: &str = "tests/compare";
+const SNAP_COMPARE: &str = "tests/snapshots/compare";
+const EXPECT_COMPARE: &str = "./snapshots/compare";
 
 fn compare(
-    tmp: &str,
+    shared_file: &str,
     v_file: &[&str],
     f: &str,
     assert: impl Fn(&SerFunction, &SerFunction, &str, &str, &str),
 ) {
+    struct ProofPath {
+        src_file: String,
+        hash_json: String,
+        hash_json_expected: String,
+    }
+
     let len = v_file.len();
     assert!(len > 1);
-    let tmp = format!("{COMPARE}/{tmp}.rs");
+    let v_path: Vec<_> = v_file
+        .iter()
+        .map(|file| ProofPath {
+            src_file: format!("{COMPARE}/{file}.rs"),
+            hash_json: format!("{SNAP_COMPARE}/{file}.json"),
+            hash_json_expected: format!("{EXPECT_COMPARE}/{file}.json"),
+        })
+        .collect();
+    let tmp = format!("{COMPARE}/{shared_file}.rs");
 
     let mut v_func = vec![];
-    for ele in v_file {
-        copy(format!("{COMPARE}/{ele}.rs"), &tmp).unwrap();
-        let text = cmd(&[&tmp]);
-        expect_file![format!("./snapshots/compare/{ele}.json")].assert_eq(&text);
+    for path in &v_path {
+        copy(&path.src_file, &tmp).unwrap();
+        let text = run_dv(&[&tmp]);
+        expect_file![&path.hash_json_expected].assert_eq(&text);
         v_func.push(get(&text, f));
     }
 
@@ -38,10 +53,19 @@ fn compare(
             assert(&v_func[i], &v_func[j], f, v_file[i], v_file[j]);
         }
     }
+
+    if let [old, new] = v_path.as_slice() {
+        let diff = run_vrs_diff(&old.hash_json, &new.hash_json);
+        let diff_json = format!("{EXPECT_COMPARE}/diff/{shared_file}.json");
+        expect_file![diff_json].assert_eq(&diff);
+    }
 }
 
 #[test]
 fn test_compare() {
+    _ = create_dir_all(SNAP_COMPARE);
+    _ = create_dir_all(format!("{SNAP_COMPARE}/diff"));
+
     fn eq(fn1: &SerFunction, fn2: &SerFunction, f: &str, f1: &str, f2: &str) {
         assert_eq!(
             fn1.hash, fn2.hash,

tests/kani_list.rs

@@ -25,13 +25,13 @@ fn validate_kani_list_json() -> Result<()> {
         expect_file![list_path].assert_debug_eq(&kani_list);
 
         // run `distributed-verification`
-        let text = cmd(&[path]);
+        let text = run_dv(&[path]);
         let v_ser_function: Vec<SerFunction> = serde_json::from_str(&text).unwrap();
         let v_proof: Vec<_> = v_ser_function.iter().filter(|f| f.is_proof()).collect();
         check_proofs(&kani_list, &v_proof).unwrap();
 
         // test `distributed-verification --check-kani-list`
-        _ = cmd(&[path, "--check-kani-list=kani-list.json"]);
+        _ = run_dv(&[path, "--check-kani-list=kani-list.json"]);
     }
 
     Ok(())

tests/proofs.rs

@@ -69,7 +69,7 @@ fn test_proofs() -> Result<()> {
     let mut v_macro = vec![];
     for (idx, path) in proofs.iter().enumerate() {
         let file_stem = file_stem(path);
-        let text = cmd(&[path.to_str().unwrap()]);
+        let text = run_dv(&[path.to_str().unwrap()]);
         v_json.push(read_proofs(&text)?);
         // collect macro generated proofs
         if file_stem.ends_with("by_macros") || file_stem.ends_with("by_nested_macros") {
@@ -111,7 +111,7 @@ fn test_compare_unique_hash() -> Result<()> {
     let mut v_json = Vec::<Vec<SerFunction>>::with_capacity(proofs.len());
     for path in &proofs {
         // let file_stem = path.file_stem().and_then(|f| f.to_str()).unwrap();
-        let text = cmd(&[path.to_str().unwrap()]);
+        let text = run_dv(&[path.to_str().unwrap()]);
         // NOTE: don't write text to json file, since compare.rs write it in a different way
         v_json.push(read_proofs(&text)?);
     }

tests/snapshots/compare/diff/contract.json

@@ -0,0 +1,77 @@
+[
+  {
+    "hash": "16423392687644375364724657870187103190",
+    "name": "std::ptr::drop_in_place::<{closure@tests/compare/contract.rs:11:5: 11:29}>",
+    "file": "library/core/src/ptr/mod.rs"
+  },
+  {
+    "hash": "16423392687644375364724657870187103190",
+    "name": "std::ptr::drop_in_place::<{closure@tests/compare/contract.rs:11:5: 11:29}>",
+    "file": "library/core/src/ptr/mod.rs"
+  },
+  {
+    "hash": "16423392687644375364724657870187103190",
+    "name": "std::ptr::drop_in_place::<{closure@tests/compare/contract.rs:11:5: 11:29}>",
+    "file": "library/core/src/ptr/mod.rs"
+  },
+  {
+    "hash": "16423392687644375364724657870187103190",
+    "name": "std::ptr::drop_in_place::<{closure@tests/compare/contract.rs:11:5: 11:29}>",
+    "file": "library/core/src/ptr/mod.rs"
+  },
+  {
+    "hash": "124569496921490884488960393718969893620",
+    "name": "verify::g",
+    "file": "tests/compare/contract.rs"
+  },
+  {
+    "hash": "73887258241161092881667616569680888010",
+    "name": "verify::g::kani_contract_mode",
+    "file": "tests/compare/contract.rs"
+  },
+  {
+    "hash": "5310357021794338182513150670169962678",
+    "name": "verify::g::kani_force_fn_once::<(), {closure@tests/compare/contract.rs:11:5: 11:29}>",
+    "file": "tests/compare/contract.rs"
+  },
+  {
+    "hash": "5310357021794338182513150670169962678",
+    "name": "verify::g::kani_force_fn_once::<(), {closure@tests/compare/contract.rs:11:5: 11:29}>",
+    "file": "tests/compare/contract.rs"
+  },
+  {
+    "hash": "5310357021794338182513150670169962678",
+    "name": "verify::g::kani_force_fn_once::<(), {closure@tests/compare/contract.rs:11:5: 11:29}>",
+    "file": "tests/compare/contract.rs"
+  },
+  {
+    "hash": "5310357021794338182513150670169962678",
+    "name": "verify::g::kani_force_fn_once::<(), {closure@tests/compare/contract.rs:11:5: 11:29}>",
+    "file": "tests/compare/contract.rs"
+  },
+  {
+    "hash": "82608928646705306325144146458835407768",
+    "name": "verify::g::kani_register_contract::<(), {closure@tests/compare/contract.rs:11:5: 11:29}>",
+    "file": "tests/compare/contract.rs"
+  },
+  {
+    "hash": "82608928646705306325144146458835407768",
+    "name": "verify::g::kani_register_contract::<(), {closure@tests/compare/contract.rs:11:5: 11:29}>",
+    "file": "tests/compare/contract.rs"
+  },
+  {
+    "hash": "82608928646705306325144146458835407768",
+    "name": "verify::g::kani_register_contract::<(), {closure@tests/compare/contract.rs:11:5: 11:29}>",
+    "file": "tests/compare/contract.rs"
+  },
+  {
+    "hash": "82608928646705306325144146458835407768",
+    "name": "verify::g::kani_register_contract::<(), {closure@tests/compare/contract.rs:11:5: 11:29}>",
+    "file": "tests/compare/contract.rs"
+  },
+  {
+    "hash": "843182267809226023016425080225293048998",
+    "name": "verify::g::{closure#0}::REENTRY",
+    "file": "tests/compare/contract.rs"
+  }
+]

tests/snapshots/compare/diff/gen_proofs_by_nested_macros.json

@@ -0,0 +1,8 @@
+[
+  {
+    "hash": "6049791535301547191723508871959023129",
+    "name": "verify::proof1",
+    "file": "tests/compare/gen_proofs_by_nested_macros.rs",
+    "proof_kind": "Standard"
+  }
+]

tests/snapshots/compare/diff/proof.json

@@ -0,0 +1,8 @@
+[
+  {
+    "hash": "1360231931955151956814099580363286591245",
+    "name": "verify::g",
+    "file": "tests/compare/proof.rs",
+    "proof_kind": "Standard"
+  }
+]

tests/stat.rs

@@ -14,7 +14,7 @@ fn stat() -> Result<()> {
 
         let path = path.to_str().unwrap();
         // run `distributed-verification path --json=false --stat`
-        let text = &cmd(&[path, "--json=false", "--stat"]);
+        let text = &run_dv(&[path, "--json=false", "--stat"]);
         // ensure this can be deserialized
         let _: Stat = serde_json::from_str(text).unwrap();
 

tests/utils.rs

@@ -7,15 +7,27 @@ pub use expect_test::{expect, expect_file};
 pub use eyre::Result;
 pub use pretty_assertions::assert_eq;
 
-pub fn cmd(args: &[&str]) -> String {
-    let mut command = Command::cargo_bin(env!("CARGO_PKG_NAME")).unwrap();
+pub fn run_dv(args: &[&str]) -> String {
+    run(env!("CARGO_PKG_NAME"), args)
+}
+
+// verify_rust_std diff --old tests/snapshots/compare/proof1.json --new tests/snapshots/compare/proof2.json --hash-json
+pub fn run_vrs_diff(old: &str, new: &str) -> String {
+    let args = &["diff", "--old", old, "--new", new, "--hash-json"];
+    run("verify_rust_std", args)
+}
+
+fn run(bin: &str, args: &[&str]) -> String {
+    let mut command = Command::cargo_bin(bin).unwrap();
     command.env("DV_LOG", "off").args(args);
     let output = command.output().unwrap();
-    assert!(
-        output.status.success(),
-        "Failed to test standard_proof.rs:\n{}",
-        std::str::from_utf8(&output.stderr).unwrap()
-    );
+    if !output.status.success() {
+        let args = args.join(" ");
+        panic!(
+            "Failed to run `{bin} {args}`\nOutput = {}",
+            std::str::from_utf8(&output.stderr).unwrap()
+        );
+    }
 
     String::from_utf8(output.stdout).unwrap()
 }