test: assert_unique_hash for proofs

cc #35

Author: zjp-CN

tests/compare.rs

@@ -1,8 +1,7 @@
-use distributed_verification::SerFunction;
 use std::fs::{copy, remove_file};
 
 mod utils;
-use utils::{assert_eq, cmd, expect_file};
+use utils::{assert_eq, *};
 
 fn get(text: &str, start: &str) -> SerFunction {
     let json = &text[text.find("[\n").unwrap()..];

tests/proofs.rs

@@ -1,8 +1,10 @@
+use indexmap::IndexMap;
+use std::path::{Path, PathBuf};
+
 mod utils;
-use utils::*;
+use utils::{assert_eq, *};
 
-#[test]
-fn test_proofs() -> eyre::Result<()> {
+pub fn get_proofs() -> Result<Vec<PathBuf>> {
     let mut proofs = vec![];
     for entry in std::fs::read_dir("tests/proofs")? {
         let entry = entry?;
@@ -13,8 +15,14 @@ fn test_proofs() -> eyre::Result<()> {
             proofs.push(path);
         }
     }
-
     proofs.sort();
+    Ok(proofs)
+}
+
+#[test]
+fn test_proofs() -> Result<()> {
+    let proofs = get_proofs()?;
+
     expect![[r#"
         [
             "tests/proofs/ad_hoc.rs",
@@ -26,15 +34,40 @@ fn test_proofs() -> eyre::Result<()> {
     "#]]
     .assert_debug_eq(&proofs);
 
+    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 json = cmd(&[&format!("tests/proofs/{file_stem}.rs")]);
-        expect_file![format!("./snapshots/{file_stem}.json")].assert_eq(&json);
+        let text = cmd(&[&format!("tests/proofs/{file_stem}.rs")]);
+        expect_file![format!("./snapshots/{file_stem}.json")].assert_eq(&text);
+        v_json.push(serde_json::from_str(&text).unwrap());
     }
 
+    assert_unique_hash(&proofs, &v_json);
+
     Ok(())
 }
 
+fn assert_unique_hash(proofs: &[PathBuf], v_json: &[Vec<SerFunction>]) {
+    let mut map = IndexMap::<&str, Vec<(&Path, &str)>>::new();
+    for (v, proof) in v_json.iter().zip(proofs) {
+        for json in v {
+            let def_id = &*json.def_id;
+            let item = (&**proof, def_id);
+            map.entry(&json.hash)
+                .and_modify(|v_item| v_item.push(item))
+                .or_insert_with(|| vec![item]);
+        }
+    }
+    for (hash, v_item) in &map {
+        let v_item_len = v_item.len();
+        assert_eq!(
+            v_item_len, 1,
+            "{hash} should only correspond to single item, but \
+             {v_item_len} items have the hash value:\n{v_item:?}",
+        );
+    }
+}
+
 #[test]
 /// Make sure latest kani is installed through cargo.
 fn kani_installed() {

tests/utils.rs

@@ -1,8 +1,11 @@
 use assert_cmd::Command;
 
-#[allow(unused_imports)] // seems a bug in clippy
+pub use distributed_verification::SerFunction;
+#[allow(unused_imports)] // seems a bug in clippy: RA only recognizes the usage in compare.rs
 pub use expect_test::{expect, expect_file};
 #[allow(unused_imports)] // seems a bug in clippy
+pub use eyre::Result;
+#[allow(unused_imports)] // seems a bug in clippy
 pub use pretty_assertions::assert_eq;
 
 pub fn cmd(args: &[&str]) -> String {