Skip to content

Commit

Permalink
test: Add profiler to recursive verification
Browse files Browse the repository at this point in the history
  • Loading branch information
Sword-Smith committed Mar 18, 2024
1 parent 3f37f2e commit 1806184
Show file tree
Hide file tree
Showing 16 changed files with 482 additions and 77 deletions.
4 changes: 2 additions & 2 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ num = "0.4"
rand = "0"
strum = { version = "0.26", features = ["derive"] }
syn = { version = "1.0", features = ["full", "extra-traits"] }
tasm-lib = { git = "https://github.com/TritonVM/tasm-lib.git", rev = "5828932c" }
tasm-lib = { git = "https://github.com/TritonVM/tasm-lib.git", rev = "2418aa26" }
quote = "1.0"

[dev-dependencies]
Expand Down
4 changes: 4 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,10 @@ bench:
bench-no-run:
cargo bench --no-run

# Run prove/verify on `verify_factorial_program`. Meant to measure recursive proof generation.
prove-recursive:
RUSTFLAGS="-C opt-level=3 -C debug-assertions=no" DYING_TO_PROVE=1 cargo t verify_factorial_program -- --test-threads=1 --nocapture

help:
@echo "usage: make [debug=1]"

Expand Down
345 changes: 345 additions & 0 deletions profiles/verify_factorial_program.profile

Large diffs are not rendered by default.

16 changes: 13 additions & 3 deletions src/tests_and_benchmarks/benchmarks.rs
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,12 @@ fn benchmark_code(
}
}

pub(crate) fn profile(function_name: String, code: Vec<LabelledInstruction>, case: BenchmarkInput) {
pub(crate) fn profile(
function_name: String,
code: Vec<LabelledInstruction>,
case: BenchmarkInput,
only_aggregated_profile: bool,
) {
// Write profile for common-case input
let nondeterminism = case.non_determinism;
let public_input = PublicInput::from(case.std_in);
Expand All @@ -62,8 +67,13 @@ pub(crate) fn profile(function_name: String, code: Vec<LabelledInstruction>, cas
"Can only profile on empty init memory for now"
);
let program: Program = Program::new(&code);
let profile =
tasm_lib::generate_full_profile(&function_name, program, &public_input, &nondeterminism);
let profile = tasm_lib::generate_full_profile(
&function_name,
program,
&public_input,
&nondeterminism,
only_aggregated_profile,
);

let mut path = PathBuf::new();
path.push("profiles");
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -126,6 +126,6 @@ mod benches {
worst_case_input,
0,
);
profile(name, code, common_case);
profile(name, code, common_case, true);
}
}
2 changes: 1 addition & 1 deletion src/tests_and_benchmarks/ozk/programs/project_euler/pe1.rs
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,6 @@ mod benches {
worst_case,
0,
);
profile(name, code, common_case);
profile(name, code, common_case, true);
}
}
2 changes: 1 addition & 1 deletion src/tests_and_benchmarks/ozk/programs/project_euler/pe2.rs
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,6 @@ mod benches {
worst_case,
0,
);
profile(name, code, common_case);
profile(name, code, common_case, true);
}
}
2 changes: 1 addition & 1 deletion src/tests_and_benchmarks/ozk/programs/project_euler/pe3.rs
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,6 @@ mod benches {
worst_case,
0,
);
profile(name, code, common_case);
profile(name, code, common_case, true);
}
}
2 changes: 1 addition & 1 deletion src/tests_and_benchmarks/ozk/programs/project_euler/pe4.rs
Original file line number Diff line number Diff line change
Expand Up @@ -114,6 +114,6 @@ mod benches {
worst_case,
0,
);
profile(name, code, common_case);
profile(name, code, common_case, true);
}
}
2 changes: 1 addition & 1 deletion src/tests_and_benchmarks/ozk/programs/project_euler/pe5.rs
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,6 @@ mod benches {
worst_case,
0,
);
profile(name, code, common_case);
profile(name, code, common_case, true);
}
}
2 changes: 1 addition & 1 deletion src/tests_and_benchmarks/ozk/programs/project_euler/pe6.rs
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,6 @@ mod benches {
worst_case,
0,
);
profile(name, code, common_case);
profile(name, code, common_case, true);
}
}
2 changes: 1 addition & 1 deletion src/tests_and_benchmarks/ozk/programs/project_euler/pe7.rs
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,6 @@ mod benches {
worst_case,
0,
);
profile(name, code, common_case);
profile(name, code, common_case, true);
}
}
2 changes: 1 addition & 1 deletion src/tests_and_benchmarks/ozk/programs/recufier/fast_ntt.rs
Original file line number Diff line number Diff line change
Expand Up @@ -233,6 +233,6 @@ mod benches {
worst_case_input,
0,
);
profile(name, code, common_case_input);
profile(name, code, common_case_input, true);
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -113,6 +113,6 @@ mod benches {
worst_case_input,
0,
);
profile(name, code, common_case_input);
profile(name, code, common_case_input, true);
}
}
Loading

0 comments on commit 1806184

Please sign in to comment.