From c035313ea2c8d3ad56683339d3534ef8bb684fa1 Mon Sep 17 00:00:00 2001 From: zjp Date: Tue, 9 Sep 2025 14:15:35 +0000 Subject: [PATCH 1/4] feat: `verify_rust_std diff --hash-json` to compare direct outputs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit $ verify_rust_std diff --old tests/snapshots/compare/proof1.json --new tests/snapshots/compare/proof2.json --hash-json [ { "hash": "1360231931955151956814099580363286591245", "name": "verify::g", "file": "tests/compare/proof.rs", "proof_kind": "Standard" } ]⏎ --- src/bin/verify_rust_std/diff.rs | 28 +++++++++++++++++++++++++--- src/diff.rs | 11 ++++++++++- src/lib.rs | 2 +- 3 files changed, 36 insertions(+), 5 deletions(-) diff --git a/src/bin/verify_rust_std/diff.rs b/src/bin/verify_rust_std/diff.rs index d200982..9c14c6d 100644 --- a/src/bin/verify_rust_std/diff.rs +++ b/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 = read_json(&self.old)?; + let new: Vec = 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 = read_json(&self.old)?; let new: Vec = 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(()) diff --git a/src/diff.rs b/src/diff.rs index 8888bd6..54dfb27 100644 --- a/src/diff.rs +++ b/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 { +pub fn diff_on_merged( + old: &[MergeHashKaniList], + new: &[MergeHashKaniList], +) -> Vec { 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 { + let set: HashSet<_> = old.iter().collect(); + new.iter().filter(|item| !set.contains(item)).cloned().collect() +} diff --git a/src/lib.rs b/src/lib.rs index 04136b8..127b033 100644 --- a/src/lib.rs +++ b/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, pub name: Box, From d38c0db0c1e9910c084f9665c534215bd3565e57 Mon Sep 17 00:00:00 2001 From: zjp Date: Wed, 10 Sep 2025 01:00:42 +0000 Subject: [PATCH 2/4] tests: utils::cmd => utils::run_dv; add utils::run_vrs --- tests/compare.rs | 2 +- tests/kani_list.rs | 4 ++-- tests/proofs.rs | 4 ++-- tests/stat.rs | 2 +- tests/utils.rs | 12 ++++++++++-- 5 files changed, 16 insertions(+), 8 deletions(-) diff --git a/tests/compare.rs b/tests/compare.rs index 949433c..e52b796 100644 --- a/tests/compare.rs +++ b/tests/compare.rs @@ -24,7 +24,7 @@ fn compare( let mut v_func = vec![]; for ele in v_file { copy(format!("{COMPARE}/{ele}.rs"), &tmp).unwrap(); - let text = cmd(&[&tmp]); + let text = run_dv(&[&tmp]); expect_file![format!("./snapshots/compare/{ele}.json")].assert_eq(&text); v_func.push(get(&text, f)); } diff --git a/tests/kani_list.rs b/tests/kani_list.rs index 38437a2..5453b71 100644 --- a/tests/kani_list.rs +++ b/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 = 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(()) diff --git a/tests/proofs.rs b/tests/proofs.rs index 076a7ff..a6aa17b 100644 --- a/tests/proofs.rs +++ b/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::>::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)?); } diff --git a/tests/stat.rs b/tests/stat.rs index c5ea50b..914d911 100644 --- a/tests/stat.rs +++ b/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(); diff --git a/tests/utils.rs b/tests/utils.rs index e0a1e4b..fedd013 100644 --- a/tests/utils.rs +++ b/tests/utils.rs @@ -7,8 +7,16 @@ 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) +} + +pub fn run_vrs(args: &[&str]) -> String { + 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!( From 9cf3ad94a14fc89bb21294379fd6d04debdfafba Mon Sep 17 00:00:00 2001 From: zjp Date: Wed, 10 Sep 2025 01:55:52 +0000 Subject: [PATCH 3/4] tests: fix utils::run error reports --- tests/utils.rs | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/tests/utils.rs b/tests/utils.rs index fedd013..1cb2eb9 100644 --- a/tests/utils.rs +++ b/tests/utils.rs @@ -19,11 +19,13 @@ 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() } From 00fbce0096b24e96017f73409d334192995bbf47 Mon Sep 17 00:00:00 2001 From: zjp Date: Wed, 10 Sep 2025 02:43:52 +0000 Subject: [PATCH 4/4] tests: add diff snapshots for proofs in compare folder --- tests/compare.rs | 38 +++++++-- tests/snapshots/compare/diff/contract.json | 77 +++++++++++++++++++ .../diff/gen_proofs_by_nested_macros.json | 8 ++ tests/snapshots/compare/diff/proof.json | 8 ++ tests/utils.rs | 4 +- 5 files changed, 127 insertions(+), 8 deletions(-) create mode 100644 tests/snapshots/compare/diff/contract.json create mode 100644 tests/snapshots/compare/diff/gen_proofs_by_nested_macros.json create mode 100644 tests/snapshots/compare/diff/proof.json diff --git a/tests/compare.rs b/tests/compare.rs index e52b796..494275a 100644 --- a/tests/compare.rs +++ b/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(); + for path in &v_path { + copy(&path.src_file, &tmp).unwrap(); let text = run_dv(&[&tmp]); - expect_file![format!("./snapshots/compare/{ele}.json")].assert_eq(&text); + 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, diff --git a/tests/snapshots/compare/diff/contract.json b/tests/snapshots/compare/diff/contract.json new file mode 100644 index 0000000..c984abd --- /dev/null +++ b/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" + } +] \ No newline at end of file diff --git a/tests/snapshots/compare/diff/gen_proofs_by_nested_macros.json b/tests/snapshots/compare/diff/gen_proofs_by_nested_macros.json new file mode 100644 index 0000000..f20afdc --- /dev/null +++ b/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" + } +] \ No newline at end of file diff --git a/tests/snapshots/compare/diff/proof.json b/tests/snapshots/compare/diff/proof.json new file mode 100644 index 0000000..8d5bec8 --- /dev/null +++ b/tests/snapshots/compare/diff/proof.json @@ -0,0 +1,8 @@ +[ + { + "hash": "1360231931955151956814099580363286591245", + "name": "verify::g", + "file": "tests/compare/proof.rs", + "proof_kind": "Standard" + } +] \ No newline at end of file diff --git a/tests/utils.rs b/tests/utils.rs index 1cb2eb9..fe871f4 100644 --- a/tests/utils.rs +++ b/tests/utils.rs @@ -11,7 +11,9 @@ pub fn run_dv(args: &[&str]) -> String { run(env!("CARGO_PKG_NAME"), args) } -pub fn run_vrs(args: &[&str]) -> String { +// 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) }