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 Option wrapping and cloning for recursive snarks
  • Loading branch information
@arthurpaulino
arthurpaulino committed Feb 13, 2024
1 parent 35a17ea commit 6862de2
Show file tree
Hide file tree
Showing 2 changed files with 76 additions and 98 deletions.
125 changes: 57 additions & 68 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,35 @@ 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();
let first_step = steps.first().expect("steps can't be empty");
assert_eq!(first_step.arity(), z0.len());

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

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

// produce a recursive SNARK
let mut recursive_snark: Option<RecursiveSNARK<E1<F>>> = None;
info!("proving {num_steps} steps");

let mut recursive_snark = RecursiveSNARK::new(
&pp.pp,
first_step,
&secondary_circuit,
z0,
&Self::z0_secondary(),
)
.map_err(ProofError::Nova)?;

let mut prove_step = |i: usize, step: &C1LEM<'a, F, C>| {
if debug {
debug_step(step, store).unwrap();
}
info!("prove_step {i}");
recursive_snark
.prove_step(&pp.pp, step, &secondary_circuit)
.unwrap();
};

// the shadowing here is voluntary
let recursive_snark = if lurk_config(None, None)
if lurk_config(None, None)
.perf
.parallelism
.recursive_steps
Expand All @@ -272,69 +309,21 @@ 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
})
.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
};

Ok(Self::Recursive(
Box::new(recursive_snark.unwrap()),
Box::new(recursive_snark),
num_steps,
PhantomData,
))
Expand Down
49 changes: 19 additions & 30 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,36 +202,29 @@ 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 debug = false;
let first_step = steps.first().expect("steps can't be empty");

let z0_primary = z0;
let z0_secondary = Self::z0_secondary();
info!("proving {} steps", steps.len());

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

let secondary_circuit = step.secondary_circuit();

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()
});
let mut recursive_snark = RecursiveSNARK::new(
&pp.pp,
first_step,
first_step,
&first_step.secondary_circuit(),
z0,
&Self::z0_secondary(),
)
.map_err(ProofError::SuperNova)?;

let mut prove_step = |i: usize, step: &C1LEM<'a, F, C>| {
if debug {
debug_step(step, store).unwrap();
}
info!("prove_step {i}");

recursive_snark
.prove_step(&pp.pp, step, &secondary_circuit)
.prove_step(&pp.pp, step, &step.secondary_circuit())
.unwrap();

recursive_snark_option = Some(recursive_snark);
};

if lurk_config(None, None)
Expand Down Expand Up @@ -291,11 +284,7 @@ impl<'a, F: CurveCycleEquipped, C: Coprocessor<F>> RecursiveSNARKTrait<F, C1LEM<
}
}

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

fn compress(self, pp: &PublicParams<F>) -> Result<Self, ProofError> {
Expand Down

0 comments on commit 6862de2

Please sign in to comment.