-
Notifications
You must be signed in to change notification settings - Fork 247
supernova implementation with naive opcode commitment for argumented circuit sequence. #204
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Closed
Closed
Changes from 84 commits
Commits
Show all changes
93 commits
Select commit
Hold shift + click to select a range
9680ce6
start SuperNova
wyattbenno777 6fc299f
setup unit test and start program counter
wyattbenno777 1335d81
experimenting with the RunningClaims selector.
wyattbenno777 be1965d
start conversion of RecursiveSNARK into NivcSnark
wyattbenno777 1227efa
theta function needs to be defined. Starting from public param genera…
wyattbenno777 369a030
RunningClaims will be a user provide Struct.
wyattbenno777 1aaba05
moving CK out
wyattbenno777 506c991
setup public params in a nice way for SuperNova.
wyattbenno777 3f70adf
starting on phi logic
wyattbenno777 d69881f
adding pci into code
wyattbenno777 917b64d
move cks out and also start on U_i and pki as described in paper.
wyattbenno777 c39dd0e
Start on SuperNova augmented circuit
wyattbenno777 af18410
work on augmented circuit2
wyattbenno777 d77f0e6
testing pci as output
wyattbenno777 0d8da59
closer to pci fin
wyattbenno777 3db8154
push notes
wyattbenno777 9c25182
more details and analysis of implementation method.
wyattbenno777 d00ffd6
change to match paper
wyattbenno777 a953b93
clarified wording
wyattbenno777 b9ea1d1
leave write up for review.
wyattbenno777 09ca660
typo
wyattbenno777 a6260f6
clarity
wyattbenno777 acb92e8
inputize progam_counter
wyattbenno777 84c94b7
start on hash of U_i
wyattbenno777 3135aec
swapping wording out for hash of Fpci' pre-image
wyattbenno777 ebdae6d
testing U_i constraints
wyattbenno777 59aefe6
need to rethink how U_i works in the circuit. Might just be a hash.
wyattbenno777 d89a33f
decided on how to represent the running instance U_i in the cicruits.
wyattbenno777 4877bb1
change to U_i is preset amount of circuits.
wyattbenno777 6614974
refactor
wyattbenno777 bbed364
got output of hash supernova from circuit
wyattbenno777 f875176
add new X2 for supernova_hash. All tests are a GO!
wyattbenno777 6f6b78e
prep for SuperNova circuit sequence checking
wyattbenno777 47b8827
generics for circuit passing
wyattbenno777 c2da773
cleanup
wyattbenno777 d3bd007
verify supernova step
wyattbenno777 3c126f7
add supernova hash witness check
hero78119 17a0c52
cleanup and bug fix
hero78119 cb0b307
add Makefile
hero78119 24080e7
fix bugs and cleanup generics
hero78119 2f2ef37
compile pass but test failed due to shape mismatch
hero78119 7ee1d7e
refactor to fit supernova implementation
hero78119 ab70de1
introduce rom concept
hero78119 b0fc5f9
constrain sequence execution by memory commitment
hero78119 76caba7
rom access commitment: program counter manipulation by step circuit
hero78119 f63e700
code cleanup
hero78119 39313e2
constrain pc[i]=z_i[x] in step circuit as well
hero78119 50847bc
remove number of arguments circuit constraint
hero78119 bf7714f
adapt latest main
hero78119 52d45e5
reuse nova nicv::prove for supernova
hero78119 9ab25b2
reuse nova runninginstance for supernova
hero78119 ce62935
more util function to serve supernova
hero78119 6ad9495
disable supernova by default
hero78119 27962c2
error pruning: arity length check in synthesis function
hero78119 a41f694
primary circuit folding can be single element
hero78119 5127517
optimise supernova proof size from 2*relax_rc1s to relax_rc1s + 1
hero78119 b20ff46
code cosmetics
hero78119 57ce58d
cleanup and reuse compute_digest, fix typo
hero78119 1be36a3
variable rename and cleanup some leftover
hero78119 d1215bc
better naming and cleanup
hero78119 ca051c0
proper naming on r1cs_shape
hero78119 34d11ff
opt memory usage, remove unnessesary clone trait
hero78119 f276690
docs decoration
hero78119 e967dc0
isolated trait/lib for supernova
hero78119 bca5eca
expose supernova module public
hero78119 a1afca6
refactor and reuse most of reference
hero78119 08a2470
optimize pc handling in step circuit, opt running instance clone
hero78119 7323e70
fix comment format
hero78119 b0765eb
retain constraint in Nova to narrow down the scope
hero78119 1efbe6c
clean up comment
hero78119 c21be47
add supernova bench
hero78119 37b4fea
almost all passed by reference in supernova recursivesnark
hero78119 66a3468
supernova soundness and clippy fix
hero78119 972ee39
fix groupname in supernova bench
hero78119 f402219
chores: polish reference usage in prove step
hero78119 996d35c
fix bug in recursive snark base case for only success on first runnin…
hero78119 5f7d4e6
merge with main branch
hero78119 5067445
simplify synthesis error handling
hero78119 b02cf87
supernova align naming convention with nova
hero78119 ebe1f08
fix soundness in supernova sequence constraints
hero78119 cd9ab49
code cosmetics based on review comments
hero78119 c9fb511
optimise util alloc_const and supernova usage
hero78119 1c47c78
code cosmetics and clean up
hero78119 ea14cab
optimize with less constriants, following-up fixing soundness on cons…
hero78119 2d3cce0
eliminate program_counter from secondary circuit ro, better error han…
hero78119 ccf0547
typo fix
hero78119 b523c40
sync with main branch
hero78119 0642cee
supernova refactor test to separate mod
hero78119 4e7ea95
clean up UnSatMsg from Nova error
hero78119 a938f29
fix soundness: empty running instance under-constraint
hero78119 e89c3ad
refactor circuit test to test module
hero78119 f76dfc2
code cosmetics
hero78119 4475884
fix soundness: use last_augmented_circuit_index consistently
hero78119 File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,329 @@ | ||
| #![allow(non_snake_case)] | ||
|
|
||
| use bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError}; | ||
| use core::marker::PhantomData; | ||
| use criterion::*; | ||
| use ff::PrimeField; | ||
| use nova_snark::{ | ||
| compute_digest, | ||
| supernova::RecursiveSNARK, | ||
| supernova::{gen_commitmentkey_by_r1cs, PublicParams, RunningClaim}, | ||
| traits::{ | ||
| circuit_supernova::{StepCircuit, TrivialTestCircuit}, | ||
| Group, | ||
| }, | ||
| }; | ||
| use std::time::Duration; | ||
|
|
||
| type G1 = pasta_curves::pallas::Point; | ||
| type G2 = pasta_curves::vesta::Point; | ||
|
|
||
| // To run these benchmarks, first download `criterion` with `cargo install cargo-criterion`. | ||
| // Then `cargo criterion --bench recursive-snark-supernova`. The results are located in `target/criterion/data/<name-of-benchmark>`. | ||
| // For flamegraphs, run `cargo criterion --bench recursive-snark-supernova --features flamegraph -- --profile-time <secs>`. | ||
| // The results are located in `target/criterion/profile/<name-of-benchmark>`. | ||
| cfg_if::cfg_if! { | ||
| if #[cfg(feature = "flamegraph")] { | ||
| criterion_group! { | ||
| name = recursive_snark_supernova; | ||
| config = Criterion::default().warm_up_time(Duration::from_millis(3000)).with_profiler(pprof::criterion::PProfProfiler::new(100, pprof::criterion::Output::Flamegraph(None))); | ||
| targets = bench_one_augmented_circuit_recursive_snark, bench_two_augmented_circuit_recursive_snark | ||
| } | ||
| } else { | ||
| criterion_group! { | ||
| name = recursive_snark_supernova; | ||
| config = Criterion::default().warm_up_time(Duration::from_millis(3000)); | ||
| targets = bench_one_augmented_circuit_recursive_snark, bench_two_augmented_circuit_recursive_snark | ||
| } | ||
| } | ||
| } | ||
|
|
||
| criterion_main!(recursive_snark_supernova); | ||
|
|
||
| fn bench_one_augmented_circuit_recursive_snark(c: &mut Criterion) { | ||
| let num_cons_verifier_circuit_primary = 9819; | ||
| // we vary the number of constraints in the step circuit | ||
| for &num_cons_in_augmented_circuit in | ||
| [9819, 16384, 32768, 65536, 131072, 262144, 524288, 1048576].iter() | ||
| { | ||
| // number of constraints in the step circuit | ||
| let num_cons = num_cons_in_augmented_circuit - num_cons_verifier_circuit_primary; | ||
|
|
||
| let mut group = c.benchmark_group(format!( | ||
| "RecursiveSNARKSuperNova-1circuit-StepCircuitSize-{num_cons}" | ||
| )); | ||
| group.sample_size(10); | ||
|
|
||
| let c_primary = NonTrivialTestCircuit::new(num_cons); | ||
| let c_secondary = TrivialTestCircuit::default(); | ||
|
|
||
| // Structuring running claims | ||
| let mut running_claim1 = RunningClaim::< | ||
| G1, | ||
| G2, | ||
| NonTrivialTestCircuit<<G1 as Group>::Scalar>, | ||
| TrivialTestCircuit<<G2 as Group>::Scalar>, | ||
| >::new(0, c_primary, c_secondary.clone(), 1); | ||
|
|
||
| let (r1cs_shape_primary, r1cs_shape_secondary) = running_claim1.get_r1cs_shape(); | ||
| let ck_primary = gen_commitmentkey_by_r1cs(r1cs_shape_primary); | ||
| let ck_secondary = gen_commitmentkey_by_r1cs(r1cs_shape_secondary); | ||
|
|
||
| // set unified ck_primary, ck_secondary and update digest | ||
| running_claim1.set_commitmentkey(ck_primary.clone(), ck_secondary.clone()); | ||
| let digest = compute_digest::<G1, PublicParams<G1, G2>>(&[running_claim1.get_publicparams()]); | ||
|
|
||
| // Bench time to produce a recursive SNARK; | ||
| // we execute a certain number of warm-up steps since executing | ||
| // the first step is cheaper than other steps owing to the presence of | ||
| // a lot of zeros in the satisfying assignment | ||
| let num_warmup_steps = 10; | ||
| let z0_primary = vec![<G1 as Group>::Scalar::from(2u64)]; | ||
| let z0_secondary = vec![<G2 as Group>::Scalar::from(2u64)]; | ||
| let initial_program_counter = <G1 as Group>::Scalar::from(0); | ||
| let mut recursive_snark_option: Option<RecursiveSNARK<G1, G2>> = None; | ||
|
|
||
| for _ in 0..num_warmup_steps { | ||
| let program_counter = recursive_snark_option | ||
| .as_ref() | ||
| .map(|recursive_snark| recursive_snark.get_program_counter()) | ||
| .unwrap_or_else(|| initial_program_counter); | ||
|
|
||
| let mut recursive_snark = recursive_snark_option.unwrap_or_else(|| { | ||
| RecursiveSNARK::iter_base_step( | ||
| &running_claim1, | ||
| digest, | ||
| program_counter, | ||
| 0, | ||
| 1, | ||
| &z0_primary, | ||
| &z0_secondary, | ||
| ) | ||
| .unwrap() | ||
| }); | ||
|
|
||
| let res = recursive_snark.prove_step(&running_claim1, &z0_primary, &z0_secondary); | ||
| if let Err(e) = &res { | ||
| println!("res failed {:?}", e); | ||
| } | ||
| assert!(res.is_ok()); | ||
| let res = recursive_snark.verify(&running_claim1, &z0_primary, &z0_secondary); | ||
| if let Err(e) = &res { | ||
| println!("res failed {:?}", e); | ||
| } | ||
| assert!(res.is_ok()); | ||
| recursive_snark_option = Some(recursive_snark) | ||
| } | ||
|
|
||
| assert!(recursive_snark_option.is_some()); | ||
| let recursive_snark = recursive_snark_option.unwrap(); | ||
|
|
||
| // Benchmark the prove time | ||
| group.bench_function("Prove", |b| { | ||
| b.iter(|| { | ||
| // produce a recursive SNARK for a step of the recursion | ||
| assert!(black_box(&mut recursive_snark.clone()) | ||
| .prove_step( | ||
| black_box(&running_claim1), | ||
| black_box(&[<G1 as Group>::Scalar::from(2u64)]), | ||
| black_box(&[<G2 as Group>::Scalar::from(2u64)]), | ||
| ) | ||
| .is_ok()); | ||
| }) | ||
| }); | ||
|
|
||
| // Benchmark the verification time | ||
| group.bench_function("Verify", |b| { | ||
| b.iter(|| { | ||
| assert!(black_box(&mut recursive_snark.clone()) | ||
| .verify( | ||
| black_box(&running_claim1), | ||
| black_box(&[<G1 as Group>::Scalar::from(2u64)]), | ||
| black_box(&[<G2 as Group>::Scalar::from(2u64)]), | ||
| ) | ||
| .is_ok()); | ||
| }); | ||
| }); | ||
| group.finish(); | ||
| } | ||
| } | ||
|
|
||
| fn bench_two_augmented_circuit_recursive_snark(c: &mut Criterion) { | ||
| let num_cons_verifier_circuit_primary = 9819; | ||
| // we vary the number of constraints in the step circuit | ||
| for &num_cons_in_augmented_circuit in | ||
| [9819, 16384, 32768, 65536, 131072, 262144, 524288, 1048576].iter() | ||
| { | ||
| // number of constraints in the step circuit | ||
| let num_cons = num_cons_in_augmented_circuit - num_cons_verifier_circuit_primary; | ||
|
|
||
| let mut group = c.benchmark_group(format!( | ||
| "RecursiveSNARKSuperNova-2circuit-StepCircuitSize-{num_cons}" | ||
| )); | ||
| group.sample_size(10); | ||
|
|
||
| let c_primary = NonTrivialTestCircuit::new(num_cons); | ||
| let c_secondary = TrivialTestCircuit::default(); | ||
|
|
||
| // Structuring running claims | ||
| let mut running_claim1 = RunningClaim::< | ||
| G1, | ||
| G2, | ||
| NonTrivialTestCircuit<<G1 as Group>::Scalar>, | ||
| TrivialTestCircuit<<G2 as Group>::Scalar>, | ||
| >::new(0, c_primary.clone(), c_secondary.clone(), 2); | ||
|
|
||
| // Structuring running claims | ||
| let mut running_claim2 = RunningClaim::< | ||
| G1, | ||
| G2, | ||
| NonTrivialTestCircuit<<G1 as Group>::Scalar>, | ||
| TrivialTestCircuit<<G2 as Group>::Scalar>, | ||
| >::new(1, c_primary, c_secondary.clone(), 2); | ||
|
|
||
| let (r1cs_shape_primary, r1cs_shape_secondary) = running_claim1.get_r1cs_shape(); | ||
| let ck_primary = gen_commitmentkey_by_r1cs(r1cs_shape_primary); | ||
| let ck_secondary = gen_commitmentkey_by_r1cs(r1cs_shape_secondary); | ||
|
|
||
| // set unified ck_primary, ck_secondary and update digest | ||
| running_claim1.set_commitmentkey(ck_primary.clone(), ck_secondary.clone()); | ||
| running_claim2.set_commitmentkey(ck_primary.clone(), ck_secondary.clone()); | ||
|
|
||
| let digest = compute_digest::<G1, PublicParams<G1, G2>>(&[ | ||
| running_claim1.get_publicparams(), | ||
| running_claim2.get_publicparams(), | ||
| ]); | ||
|
|
||
| // Bench time to produce a recursive SNARK; | ||
| // we execute a certain number of warm-up steps since executing | ||
| // the first step is cheaper than other steps owing to the presence of | ||
| // a lot of zeros in the satisfying assignment | ||
| let num_warmup_steps = 10; | ||
| let z0_primary = vec![<G1 as Group>::Scalar::from(2u64)]; | ||
| let z0_secondary = vec![<G2 as Group>::Scalar::from(2u64)]; | ||
| let initial_program_counter = <G1 as Group>::Scalar::from(0); | ||
| let mut recursive_snark_option: Option<RecursiveSNARK<G1, G2>> = None; | ||
| let mut selected_augmented_circuit = 0; | ||
|
|
||
| for _ in 0..num_warmup_steps { | ||
| let program_counter = recursive_snark_option | ||
| .as_ref() | ||
| .map(|recursive_snark| recursive_snark.get_program_counter()) | ||
| .unwrap_or_else(|| initial_program_counter); | ||
|
|
||
| let mut recursive_snark = recursive_snark_option.unwrap_or_else(|| { | ||
| RecursiveSNARK::iter_base_step( | ||
| &running_claim1, | ||
| digest, | ||
| program_counter, | ||
| 0, | ||
| 2, | ||
| &z0_primary, | ||
| &z0_secondary, | ||
| ) | ||
| .unwrap() | ||
| }); | ||
|
|
||
| if selected_augmented_circuit == 0 { | ||
| let res = recursive_snark.prove_step(&running_claim1, &z0_primary, &z0_secondary); | ||
| if let Err(e) = &res { | ||
| println!("res failed {:?}", e); | ||
| } | ||
| assert!(res.is_ok()); | ||
| let res = recursive_snark.verify(&running_claim1, &z0_primary, &z0_secondary); | ||
| if let Err(e) = &res { | ||
| println!("res failed {:?}", e); | ||
| } | ||
| assert!(res.is_ok()); | ||
| } else if selected_augmented_circuit == 1 { | ||
| let res = recursive_snark.prove_step(&running_claim2, &z0_primary, &z0_secondary); | ||
| if let Err(e) = &res { | ||
| println!("res failed {:?}", e); | ||
| } | ||
| assert!(res.is_ok()); | ||
| let res = recursive_snark.verify(&running_claim2, &z0_primary, &z0_secondary); | ||
| if let Err(e) = &res { | ||
| println!("res failed {:?}", e); | ||
| } | ||
| assert!(res.is_ok()); | ||
| } else { | ||
| unimplemented!() | ||
| } | ||
| selected_augmented_circuit = (selected_augmented_circuit + 1) % 2; | ||
| recursive_snark_option = Some(recursive_snark) | ||
| } | ||
|
|
||
| assert!(recursive_snark_option.is_some()); | ||
| let recursive_snark = recursive_snark_option.unwrap(); | ||
|
|
||
| // Benchmark the prove time | ||
| group.bench_function("Prove", |b| { | ||
| b.iter(|| { | ||
| // produce a recursive SNARK for a step of the recursion | ||
| assert!(black_box(&mut recursive_snark.clone()) | ||
| .prove_step( | ||
| black_box(&running_claim1), | ||
| black_box(&[<G1 as Group>::Scalar::from(2u64)]), | ||
| black_box(&[<G2 as Group>::Scalar::from(2u64)]), | ||
| ) | ||
| .is_ok()); | ||
| }) | ||
| }); | ||
|
|
||
| // Benchmark the verification time | ||
| group.bench_function("Verify", |b| { | ||
| b.iter(|| { | ||
| assert!(black_box(&mut recursive_snark.clone()) | ||
| .verify( | ||
| black_box(&running_claim1), | ||
| black_box(&[<G1 as Group>::Scalar::from(2u64)]), | ||
| black_box(&[<G2 as Group>::Scalar::from(2u64)]), | ||
| ) | ||
| .is_ok()); | ||
| }); | ||
| }); | ||
| group.finish(); | ||
| } | ||
| } | ||
|
|
||
| #[derive(Clone, Debug, Default)] | ||
| struct NonTrivialTestCircuit<F: PrimeField> { | ||
| num_cons: usize, | ||
| _p: PhantomData<F>, | ||
| } | ||
|
|
||
| impl<F> NonTrivialTestCircuit<F> | ||
| where | ||
| F: PrimeField, | ||
| { | ||
| pub fn new(num_cons: usize) -> Self { | ||
| Self { | ||
| num_cons, | ||
| _p: Default::default(), | ||
| } | ||
| } | ||
| } | ||
| impl<F> StepCircuit<F> for NonTrivialTestCircuit<F> | ||
| where | ||
| F: PrimeField, | ||
| { | ||
| fn arity(&self) -> usize { | ||
| 1 | ||
| } | ||
|
|
||
| fn synthesize<CS: ConstraintSystem<F>>( | ||
| &self, | ||
| cs: &mut CS, | ||
| pc: &AllocatedNum<F>, | ||
| z: &[AllocatedNum<F>], | ||
| ) -> Result<(AllocatedNum<F>, Vec<AllocatedNum<F>>), SynthesisError> { | ||
| // Consider a an equation: `x^2 = y`, where `x` and `y` are respectively the input and output. | ||
| let mut x = z[0].clone(); | ||
| let mut y = x.clone(); | ||
| for i in 0..self.num_cons { | ||
| y = x.square(cs.namespace(|| format!("x_sq_{i}")))?; | ||
| x = y.clone(); | ||
| } | ||
| Ok((pc.clone(), vec![y])) | ||
| } | ||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.