Skip to content
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

supernova implementation with naive opcode commitment for argumented circuit sequence. #204

Closed
wants to merge 93 commits into from
Closed
Show file tree
Hide file tree
Changes from 89 commits
Commits
Show all changes
93 commits
Select commit Hold shift + click to select a range
9680ce6
start SuperNova
wyattbenno777 Jun 29, 2023
6fc299f
setup unit test and start program counter
wyattbenno777 Jun 29, 2023
1335d81
experimenting with the RunningClaims selector.
wyattbenno777 Jun 29, 2023
be1965d
start conversion of RecursiveSNARK into NivcSnark
wyattbenno777 Jun 30, 2023
1227efa
theta function needs to be defined. Starting from public param genera…
wyattbenno777 Jun 30, 2023
369a030
RunningClaims will be a user provide Struct.
wyattbenno777 Jul 1, 2023
1aaba05
moving CK out
wyattbenno777 Jul 3, 2023
506c991
setup public params in a nice way for SuperNova.
wyattbenno777 Jul 3, 2023
3f70adf
starting on phi logic
wyattbenno777 Jul 4, 2023
d69881f
adding pci into code
wyattbenno777 Jul 4, 2023
917b64d
move cks out and also start on U_i and pki as described in paper.
wyattbenno777 Jul 4, 2023
c39dd0e
Start on SuperNova augmented circuit
wyattbenno777 Jul 5, 2023
af18410
work on augmented circuit2
wyattbenno777 Jul 5, 2023
d77f0e6
testing pci as output
wyattbenno777 Jul 5, 2023
0d8da59
closer to pci fin
wyattbenno777 Jul 5, 2023
3db8154
push notes
wyattbenno777 Jul 5, 2023
9c25182
more details and analysis of implementation method.
wyattbenno777 Jul 6, 2023
d00ffd6
change to match paper
wyattbenno777 Jul 6, 2023
a953b93
clarified wording
wyattbenno777 Jul 6, 2023
b9ea1d1
leave write up for review.
wyattbenno777 Jul 6, 2023
09ca660
typo
wyattbenno777 Jul 6, 2023
a6260f6
clarity
wyattbenno777 Jul 6, 2023
acb92e8
inputize progam_counter
wyattbenno777 Jul 7, 2023
84c94b7
start on hash of U_i
wyattbenno777 Jul 7, 2023
3135aec
swapping wording out for hash of Fpci' pre-image
wyattbenno777 Jul 7, 2023
ebdae6d
testing U_i constraints
wyattbenno777 Jul 7, 2023
59aefe6
need to rethink how U_i works in the circuit. Might just be a hash.
wyattbenno777 Jul 7, 2023
d89a33f
decided on how to represent the running instance U_i in the cicruits.
wyattbenno777 Jul 9, 2023
4877bb1
change to U_i is preset amount of circuits.
wyattbenno777 Jul 9, 2023
6614974
refactor
wyattbenno777 Jul 9, 2023
bbed364
got output of hash supernova from circuit
wyattbenno777 Jul 10, 2023
f875176
add new X2 for supernova_hash. All tests are a GO!
wyattbenno777 Jul 10, 2023
6f6b78e
prep for SuperNova circuit sequence checking
wyattbenno777 Jul 11, 2023
47b8827
generics for circuit passing
wyattbenno777 Jul 11, 2023
c2da773
cleanup
wyattbenno777 Jul 11, 2023
d3bd007
verify supernova step
wyattbenno777 Jul 11, 2023
3c126f7
add supernova hash witness check
hero78119 Jul 11, 2023
17a0c52
cleanup and bug fix
hero78119 Jul 12, 2023
cb0b307
add Makefile
hero78119 Jul 12, 2023
24080e7
fix bugs and cleanup generics
hero78119 Jul 12, 2023
2f2ef37
compile pass but test failed due to shape mismatch
hero78119 Jul 12, 2023
7ee1d7e
refactor to fit supernova implementation
hero78119 Jul 14, 2023
ab70de1
introduce rom concept
hero78119 Jul 15, 2023
b0fc5f9
constrain sequence execution by memory commitment
hero78119 Jul 15, 2023
76caba7
rom access commitment: program counter manipulation by step circuit
hero78119 Jul 16, 2023
f63e700
code cleanup
hero78119 Jul 16, 2023
39313e2
constrain pc[i]=z_i[x] in step circuit as well
hero78119 Jul 16, 2023
50847bc
remove number of arguments circuit constraint
hero78119 Jul 16, 2023
bf7714f
adapt latest main
hero78119 Jul 16, 2023
52d45e5
reuse nova nicv::prove for supernova
hero78119 Jul 16, 2023
9ab25b2
reuse nova runninginstance for supernova
hero78119 Jul 16, 2023
ce62935
more util function to serve supernova
hero78119 Jul 16, 2023
6ad9495
disable supernova by default
hero78119 Jul 16, 2023
27962c2
error pruning: arity length check in synthesis function
hero78119 Jul 17, 2023
a41f694
primary circuit folding can be single element
hero78119 Jul 18, 2023
5127517
optimise supernova proof size from 2*relax_rc1s to relax_rc1s + 1
hero78119 Jul 18, 2023
b20ff46
code cosmetics
hero78119 Jul 19, 2023
57ce58d
cleanup and reuse compute_digest, fix typo
hero78119 Jul 19, 2023
1be36a3
variable rename and cleanup some leftover
hero78119 Jul 19, 2023
d1215bc
better naming and cleanup
hero78119 Jul 19, 2023
ca051c0
proper naming on r1cs_shape
hero78119 Jul 19, 2023
34d11ff
opt memory usage, remove unnessesary clone trait
hero78119 Jul 19, 2023
f276690
docs decoration
hero78119 Jul 19, 2023
e967dc0
isolated trait/lib for supernova
hero78119 Jul 19, 2023
bca5eca
expose supernova module public
hero78119 Jul 20, 2023
a1afca6
refactor and reuse most of reference
hero78119 Jul 20, 2023
08a2470
optimize pc handling in step circuit, opt running instance clone
hero78119 Jul 20, 2023
7323e70
fix comment format
hero78119 Jul 20, 2023
b0765eb
retain constraint in Nova to narrow down the scope
hero78119 Jul 21, 2023
1efbe6c
clean up comment
hero78119 Jul 21, 2023
c21be47
add supernova bench
hero78119 Jul 21, 2023
37b4fea
almost all passed by reference in supernova recursivesnark
hero78119 Jul 21, 2023
66a3468
supernova soundness and clippy fix
hero78119 Jul 23, 2023
972ee39
fix groupname in supernova bench
hero78119 Jul 26, 2023
f402219
chores: polish reference usage in prove step
hero78119 Jul 26, 2023
996d35c
fix bug in recursive snark base case for only success on first runnin…
hero78119 Aug 4, 2023
5f7d4e6
merge with main branch
hero78119 Aug 8, 2023
5067445
simplify synthesis error handling
hero78119 Aug 3, 2023
b02cf87
supernova align naming convention with nova
hero78119 Aug 8, 2023
ebe1f08
fix soundness in supernova sequence constraints
hero78119 Aug 10, 2023
cd9ab49
code cosmetics based on review comments
hero78119 Aug 10, 2023
c9fb511
optimise util alloc_const and supernova usage
hero78119 Aug 10, 2023
1c47c78
code cosmetics and clean up
hero78119 Aug 10, 2023
ea14cab
optimize with less constriants, following-up fixing soundness on cons…
hero78119 Aug 10, 2023
2d3cce0
eliminate program_counter from secondary circuit ro, better error han…
hero78119 Aug 14, 2023
ccf0547
typo fix
hero78119 Aug 16, 2023
b523c40
sync with main branch
hero78119 Aug 16, 2023
0642cee
supernova refactor test to separate mod
hero78119 Aug 16, 2023
4e7ea95
clean up UnSatMsg from Nova error
hero78119 Aug 16, 2023
a938f29
fix soundness: empty running instance under-constraint
hero78119 Aug 16, 2023
e89c3ad
refactor circuit test to test module
hero78119 Aug 16, 2023
f76dfc2
code cosmetics
hero78119 Aug 16, 2023
4475884
fix soundness: use last_augmented_circuit_index consistently
hero78119 Aug 17, 2023
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
7 changes: 7 additions & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ byteorder = "1.4.3"
thiserror = "1.0"
halo2curves = { version = "0.4.0", features = ["derive_serde"] }
group = "0.13.0"
log = "0.4.17"

[target.'cfg(any(target_arch = "x86_64", target_arch = "aarch64"))'.dependencies]
pasta-msm = { version = "0.1.4" }
Expand Down Expand Up @@ -68,10 +69,16 @@ harness = false
name = "sha256"
harness = false

[[bench]]
name = "recursive-snark-supernova"
harness = false
required-features = ["supernova"]

hero78119 marked this conversation as resolved.
Show resolved Hide resolved
[features]
default = []
# Compiles in portable mode, w/o ISA extensions => binary can be executed on all systems.
portable = ["pasta-msm/portable"]
cuda = ["neptune/cuda", "neptune/pasta", "neptune/arity24"]
opencl = ["neptune/opencl", "neptune/pasta", "neptune/arity24"]
flamegraph = ["pprof/flamegraph", "pprof/criterion"]
supernova = []
329 changes: 329 additions & 0 deletions benches/recursive-snark-supernova.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,329 @@
#![allow(non_snake_case)]

use bellpepper_core::{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]))
}
}
2 changes: 1 addition & 1 deletion src/bellpepper/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ mod tests {
// First create the shape
let mut cs: ShapeCS<G> = ShapeCS::new();
let _ = synthesize_alloc_bit(&mut cs);
let (shape, ck) = cs.r1cs_shape();
let (shape, ck) = cs.r1cs_shape_with_commitmentkey();

// Now get the assignment
let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
Expand Down
15 changes: 10 additions & 5 deletions src/bellpepper/r1cs.rs
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,14 @@ pub trait NovaWitness<G: Group> {
/// `NovaShape` provides methods for acquiring `R1CSShape` and `CommitmentKey` from implementers.
pub trait NovaShape<G: Group> {
/// Return an appropriate `R1CSShape` and `CommitmentKey` structs.
fn r1cs_shape(&self) -> (R1CSShape<G>, CommitmentKey<G>);
fn r1cs_shape_with_commitmentkey(&self) -> (R1CSShape<G>, CommitmentKey<G>) {
let S = self.r1cs_shape();
let ck = R1CS::<G>::commitment_key(&S);

(S, ck)
}
/// Return an appropriate `R1CSShape`.
fn r1cs_shape(&self) -> R1CSShape<G>;
}

impl<G: Group> NovaWitness<G> for SatisfyingAssignment<G> {
Expand All @@ -51,7 +58,7 @@ macro_rules! impl_nova_shape {
where
G::Scalar: PrimeField,
{
fn r1cs_shape(&self) -> (R1CSShape<G>, CommitmentKey<G>) {
fn r1cs_shape(&self) -> R1CSShape<G> {
let mut A: Vec<(usize, usize, G::Scalar)> = Vec::new();
let mut B: Vec<(usize, usize, G::Scalar)> = Vec::new();
let mut C: Vec<(usize, usize, G::Scalar)> = Vec::new();
Expand Down Expand Up @@ -81,9 +88,7 @@ macro_rules! impl_nova_shape {
res.unwrap()
};

let ck = R1CS::<G>::commitment_key(&S);

(S, ck)
S
}
}
};
Expand Down