Skip to content

Commit

Permalink
chore: simplify and homogenize proving code for Nova and SuperNova pr…
Browse files Browse the repository at this point in the history 
…oofs

* Remove code duplication in Nova proving
* Factor out and reuse debugging code that was triggered only for Nova proving without "parallel steps"
* Remove the cloning of recursive snarks on SuperNova
  • Loading branch information
@arthurpaulino
arthurpaulino committed Feb 13, 2024
1 parent 35a17ea commit a5a504a
Show file tree
Hide file tree
Showing 2 changed files with 99 additions and 101 deletions.
131 changes: 64 additions & 67 deletions src/proof/nova.rs
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
use bellpepper_core::{num::AllocatedNum, ConstraintSystem};
use bellpepper_core::{num::AllocatedNum, ConstraintSystem, SynthesisError};
use halo2curves::bn256::Fr as Bn256Scalar;
use nova::{
errors::NovaError,
Expand All @@ -18,14 +18,15 @@ use std::{
marker::PhantomData,
sync::{Arc, Mutex},
};
use tracing::info;

use crate::{
config::lurk_config,
coprocessor::Coprocessor,
error::ProofError,
eval::lang::Lang,
field::LurkField,
lem::{interpreter::Frame, pointers::Ptr, store::Store},
lem::{interpreter::Frame, multiframe::MultiFrame, pointers::Ptr, store::Store},
proof::{supernova::FoldingConfig, FrameLike, Prover},
};

Expand Down Expand Up @@ -223,6 +224,29 @@ pub fn circuits<'a, F: CurveCycleEquipped, C: Coprocessor<F> + 'a>(
)
}

/// For debugging purposes, synthesize the circuit and check that the constraint
/// system is satisfied
#[inline]
pub(crate) fn debug_step<F: LurkField, C: Coprocessor<F>>(
circuit: &MultiFrame<'_, F, C>,
store: &Store<F>,
) -> Result<(), SynthesisError> {
use bellpepper_core::test_cs::TestConstraintSystem;
let mut cs = TestConstraintSystem::<F>::new();

let zi = store.to_scalar_vector(circuit.input());
let zi_allocated: Vec<_> = zi
.iter()
.enumerate()
.map(|(i, x)| AllocatedNum::alloc(cs.namespace(|| format!("z{i}_1")), || Ok(*x)))
.collect::<Result<_, _>>()?;

circuit.synthesize(&mut cs, zi_allocated.as_slice())?;

assert!(cs.is_satisfied());
Ok(())
}

impl<'a, F: CurveCycleEquipped, C: Coprocessor<F>> RecursiveSNARKTrait<F, C1LEM<'a, F, C>>
for Proof<F, C1LEM<'a, F, C>>
{
Expand All @@ -237,22 +261,41 @@ impl<'a, F: CurveCycleEquipped, C: Coprocessor<F>> RecursiveSNARKTrait<F, C1LEM<
steps: Vec<C1LEM<'a, F, C>>,
store: &Store<F>,
) -> Result<Self, ProofError> {
assert!(!steps.is_empty());
assert_eq!(steps[0].arity(), z0.len());
let debug = false;
let z0_primary = z0;
let z0_secondary = Self::z0_secondary();
assert_eq!(steps[0].arity(), z0.len());

let circuit_secondary = TrivialCircuit::default();
let secondary_circuit = TrivialCircuit::default();

let num_steps = steps.len();
tracing::debug!("steps.len: {num_steps}");
info!("proving {num_steps} steps");

// produce a recursive SNARK
let mut recursive_snark: Option<RecursiveSNARK<E1<F>>> = None;
let mut recursive_snark_option: Option<RecursiveSNARK<E1<F>>> = None;

// the shadowing here is voluntary
let recursive_snark = if lurk_config(None, None)
// a closure would capture (and move) `recursive_snark_option`
macro_rules! prove_step {
($i:expr, $step:expr) => {
if debug {
debug_step($step, store).unwrap();
}
let mut recursive_snark = recursive_snark_option.unwrap_or_else(|| {
RecursiveSNARK::new(
&pp.pp,
$step,
&secondary_circuit,
z0,
&Self::z0_secondary(),
)
.expect("failed to construct initial recursive SNARK")
});
info!("prove_step {}", $i);
recursive_snark
.prove_step(&pp.pp, $step, &secondary_circuit)
.unwrap();
recursive_snark_option = Some(recursive_snark);
};
}

recursive_snark_option = if lurk_config(None, None)
.perf
.parallelism
.recursive_steps
Expand All @@ -272,69 +315,23 @@ impl<'a, F: CurveCycleEquipped, C: Coprocessor<F>> RecursiveSNARKTrait<F, C1LEM<
});
});

for circuit_primary in cc.iter() {
let mut circuit_primary = circuit_primary.lock().unwrap();

let mut r_snark = recursive_snark.unwrap_or_else(|| {
RecursiveSNARK::new(
&pp.pp,
&*circuit_primary,
&circuit_secondary,
z0_primary,
&z0_secondary,
)
.expect("Failed to construct initial recursive snark")
});
r_snark
.prove_step(&pp.pp, &*circuit_primary, &circuit_secondary)
.expect("failure to prove Nova step");
circuit_primary.clear_cached_witness();
recursive_snark = Some(r_snark);
for (i, step) in cc.iter().enumerate() {
let mut step = step.lock().unwrap();
prove_step!(i, &*step);
step.clear_cached_witness();
}
recursive_snark
recursive_snark_option
})
.unwrap()
} else {
for circuit_primary in steps.iter() {
if debug {
// For debugging purposes, synthesize the circuit and check that the constraint system is satisfied.
use bellpepper_core::test_cs::TestConstraintSystem;
let mut cs = TestConstraintSystem::<F>::new();

let zi = store.to_scalar_vector(circuit_primary.input());
let zi_allocated: Vec<_> = zi
.iter()
.enumerate()
.map(|(i, x)| {
AllocatedNum::alloc(cs.namespace(|| format!("z{i}_1")), || Ok(*x))
})
.collect::<Result<_, _>>()?;

circuit_primary.synthesize(&mut cs, zi_allocated.as_slice())?;

assert!(cs.is_satisfied());
}

let mut r_snark = recursive_snark.unwrap_or_else(|| {
RecursiveSNARK::new(
&pp.pp,
circuit_primary,
&circuit_secondary,
z0_primary,
&z0_secondary,
)
.expect("Failed to construct initial recursive snark")
});
r_snark
.prove_step(&pp.pp, circuit_primary, &circuit_secondary)
.expect("failure to prove Nova step");
recursive_snark = Some(r_snark);
for (i, step) in steps.iter().enumerate() {
prove_step!(i, step);
}
recursive_snark
recursive_snark_option
};

Ok(Self::Recursive(
Box::new(recursive_snark.unwrap()),
Box::new(recursive_snark_option.expect("RecursiveSNARK missing")),
num_steps,
PhantomData,
))
Expand Down
69 changes: 35 additions & 34 deletions src/proof/supernova.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ use crate::{
field::LurkField,
lem::{interpreter::Frame, pointers::Ptr, store::Store},
proof::{
nova::{CurveCycleEquipped, Dual, NovaCircuitShape, E1},
nova::{debug_step, CurveCycleEquipped, Dual, NovaCircuitShape, E1},
Prover, RecursiveSNARKTrait,
},
};
Expand Down Expand Up @@ -202,39 +202,39 @@ impl<'a, F: CurveCycleEquipped, C: Coprocessor<F>> RecursiveSNARKTrait<F, C1LEM<
steps: Vec<C1LEM<'a, F, C>>,
store: &Store<F>,
) -> Result<Self, ProofError> {
let mut recursive_snark_option: Option<RecursiveSNARK<E1<F>>> = None;

let z0_primary = z0;
let z0_secondary = Self::z0_secondary();

let mut prove_step = |i: usize, step: &C1LEM<'a, F, C>| {
info!("prove_recursively, step {i}");
let debug = false;

let secondary_circuit = step.secondary_circuit();
info!("proving {} steps", steps.len());

let mut recursive_snark = recursive_snark_option.clone().unwrap_or_else(|| {
info!("RecursiveSnark::new {i}");
RecursiveSNARK::new(
&pp.pp,
step,
step,
&secondary_circuit,
z0_primary,
&z0_secondary,
)
.unwrap()
});

info!("prove_step {i}");

recursive_snark
.prove_step(&pp.pp, step, &secondary_circuit)
.unwrap();
let mut recursive_snark_option: Option<RecursiveSNARK<E1<F>>> = None;

recursive_snark_option = Some(recursive_snark);
};
// a closure would capture (and move) `recursive_snark_option`
macro_rules! prove_step {
($i:expr, $step:expr) => {
if debug {
debug_step($step, store).unwrap();
}
let secondary_circuit = $step.secondary_circuit();
let mut recursive_snark = recursive_snark_option.unwrap_or_else(|| {
RecursiveSNARK::new(
&pp.pp,
$step,
$step,
&secondary_circuit,
z0,
&Self::z0_secondary(),
)
.expect("failed to construct initial recursive SNARK")
});
info!("prove_step {}", $i);
recursive_snark
.prove_step(&pp.pp, $step, &secondary_circuit)
.unwrap();
recursive_snark_option = Some(recursive_snark);
};
}

if lurk_config(None, None)
recursive_snark_option = if lurk_config(None, None)
.perf
.parallelism
.recursive_steps
Expand Down Expand Up @@ -280,18 +280,19 @@ impl<'a, F: CurveCycleEquipped, C: Coprocessor<F>> RecursiveSNARKTrait<F, C1LEM<

for (i, (_, step)) in cc.iter().enumerate() {
let mut step = step.lock().unwrap();
prove_step(i, &step);
prove_step!(i, &*step);
step.clear_cached_witness();
}
recursive_snark_option
})
.unwrap()
} else {
for (i, step) in steps.iter().enumerate() {
prove_step(i, step);
prove_step!(i, step);
}
}
recursive_snark_option
};

// This probably should be made unnecessary.
Ok(Self::Recursive(
Box::new(recursive_snark_option.expect("RecursiveSNARK missing")),
PhantomData,
Expand Down

0 comments on commit a5a504a

Please sign in to comment.