test: compare contracts to ensure adding unrelated contracts has no impact

Ref: #18

NOTE: the hash value differs, but callee_sorted_by_file_func is
identical.

thread 'compare_contract' panicked at tests/snapshots.rs:78:5:
assertion failed: `(left == right)`

Diff < left / right > :
<929236091286910200016542852190015891876
>160785969163118787202231336083974075582

Author: zjp-CN

Cargo.lock

@@ -21,6 +21,7 @@ tracing-error = "0.2"
 [dev-dependencies]
 assert_cmd = "2.0.16"
 expect-test = "1.5.1"
+pretty_assertions = "1.4.1"
 
 [lints.rust]
 unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

Cargo.toml

@@ -24,3 +24,13 @@ pub struct Callee {
     pub file: String,
     pub func: String,
 }
+
+impl SerFunction {
+    /// Even though callees are in insertion order, to make them easy to check,
+    /// sort by file and function.
+    pub fn callee_sorted_by_file_func(&self) -> Vec<[&str; 2]> {
+        let mut callees: Vec<_> = self.callees.iter().collect();
+        callees.sort_by(|a, b| (&a.file, &a.func).cmp(&(&b.file, &b.func)));
+        callees.into_iter().map(|c| [&*c.file, &*c.func]).collect()
+    }
+}

src/lib.rs

@@ -0,0 +1,10 @@
+#[cfg(kani)]
+mod verify {
+    #[kani::requires(a > 0)]
+    pub fn contract(a: u8) {}
+
+    #[kani::proof]
+    pub fn f() {
+        contract(0);
+    }
+}

tests/compare/contract1.rs

@@ -0,0 +1,13 @@
+#[cfg(kani)]
+mod verify {
+    #[kani::requires(a > 0)]
+    pub fn contract(a: u8) {}
+
+    #[kani::proof]
+    pub fn f() {
+        contract(0);
+    }
+
+    #[kani::requires(a > 0)]
+    pub fn g(a: u8) {}
+}

tests/compare/contract2.rs

@@ -1,6 +1,7 @@
 use assert_cmd::Command;
 use distributed_verification::SerFunction;
 use expect_test::expect_file;
+use pretty_assertions::assert_eq;
 use std::fs::{copy, remove_file};
 
 fn cmd(args: &[&str]) -> String {
@@ -26,9 +27,10 @@ fn standard_proofs_with_contracts() {
     expect_file!["./snapshots/standard_proofs_with_contracts.json"].assert_eq(&json);
 }
 
-fn get_hash(text: &str, start: &str) -> String {
-    let v: Vec<SerFunction> = serde_json::from_str(text).unwrap();
-    v.into_iter().find(|f| f.func.starts_with(start)).unwrap().hash
+fn get(text: &str, start: &str) -> SerFunction {
+    let json = &text[text.find("[\n").unwrap()..];
+    let v: Vec<SerFunction> = serde_json::from_str(json).unwrap();
+    v.into_iter().find(|f| f.func.starts_with(start)).unwrap()
 }
 
 #[test]
@@ -49,5 +51,29 @@ fn compare_proof() {
     let f = "pub fn f()";
     // For the same proof (w.r.t same path and body),
     // the hash value must be the same.
-    assert_eq!(get_hash(text1, f), get_hash(text2, f));
+    assert_eq!(get(text1, f).hash, get(text2, f).hash);
+}
+
+#[test]
+fn compare_contract() {
+    let file = "tests/compare/contract.rs";
+
+    copy("tests/compare/contract1.rs", file).unwrap();
+    let text1 = &cmd(&["tests/compare/contract.rs"]);
+    expect_file!["./snapshots/contract1.json"].assert_eq(text1);
+
+    copy("tests/compare/contract2.rs", file).unwrap();
+    let text2 = &cmd(&["tests/compare/contract.rs"]);
+    expect_file!["./snapshots/contract2.json"].assert_eq(text2);
+
+    remove_file(file).unwrap();
+
+    let f = "pub fn f()";
+    let f1 = get(text1, f);
+    let f2 = get(text2, f);
+    let callees1 = f1.callee_sorted_by_file_func();
+    let callees2 = f2.callee_sorted_by_file_func();
+
+    assert_eq!(callees1, callees2);
+    assert_eq!(f1.hash, f2.hash);
 }