Skip to content

Commit

Permalink
Add non-deterministic ivc test. (#92)
Browse files Browse the repository at this point in the history
Co-authored-by: porcuquine <porcuquine@users.noreply.github.com>
  • Loading branch information
porcuquine and porcuquine committed Nov 2, 2023
1 parent f81bd4c commit 16cfdff
Show file tree
Hide file tree
Showing 4 changed files with 315 additions and 8 deletions.
4 changes: 4 additions & 0 deletions benches/recursive-snark-supernova.rs
Original file line number Diff line number Diff line change
Expand Up @@ -339,6 +339,10 @@ where
1
}

fn circuit_index(&self) -> usize {
0
}

fn synthesize<CS: ConstraintSystem<F>>(
&self,
cs: &mut CS,
Expand Down
11 changes: 6 additions & 5 deletions src/supernova/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -168,8 +168,8 @@ where
C2: StepCircuit<G2::Scalar>,
{
/// Construct a new [PublicParams]
pub fn new<NC: NonUniformCircuit<G1, G2, C1, C2>>(non_unifrom_circuit: &NC) -> Self {
let num_circuits = non_unifrom_circuit.num_circuits();
pub fn new<NC: NonUniformCircuit<G1, G2, C1, C2>>(non_uniform_circuit: &NC) -> Self {
let num_circuits = non_uniform_circuit.num_circuits();

let augmented_circuit_params_primary =
SuperNovaAugmentedCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS, true);
Expand All @@ -179,7 +179,7 @@ where

let circuit_shapes = (0..num_circuits)
.map(|i| {
let c_primary = non_unifrom_circuit.primary_circuit(i);
let c_primary = non_uniform_circuit.primary_circuit(i);
let F_arity = c_primary.arity();
// Initialize ck for the primary
let circuit_primary: SuperNovaAugmentedCircuit<'_, G2, C1> = SuperNovaAugmentedCircuit::new(
Expand All @@ -191,6 +191,7 @@ where
);
let mut cs: ShapeCS<G1> = ShapeCS::new();
let _ = circuit_primary.synthesize(&mut cs);

// We use the largest commitment_key for all instances
let r1cs_shape_primary = cs.r1cs_shape();
CircuitShape::new(r1cs_shape_primary, F_arity)
Expand All @@ -202,7 +203,7 @@ where
let augmented_circuit_params_secondary =
SuperNovaAugmentedCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS, false);
let ro_consts_secondary: ROConstants<G2> = ROConstants::<G2>::default();
let c_secondary = non_unifrom_circuit.secondary_circuit();
let c_secondary = non_uniform_circuit.secondary_circuit();
let F_arity_secondary = c_secondary.arity();
let ro_consts_circuit_secondary: ROConstantsCircuit<G1> = ROConstantsCircuit::<G1>::default();

Expand Down Expand Up @@ -615,7 +616,7 @@ where

let (l_u_primary, l_w_primary) = cs_primary
.r1cs_instance_and_witness(&pp[circuit_index].r1cs_shape, &pp.ck_primary)
.map_err(|_| SuperNovaError::NovaError(NovaError::UnSat))?;
.map_err(SuperNovaError::NovaError)?;

// Split into `if let`/`else` statement
// to avoid `returns a value referencing data owned by closure` error on `&RelaxedR1CSInstance::default` and `RelaxedR1CSWitness::default`
Expand Down
296 changes: 296 additions & 0 deletions src/supernova/test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -733,3 +733,299 @@ fn test_supernova_pp_digest() {
"3ae4759aa0338bcc6ac11b456c17803467a1f44364992e3f1a0c6344b0135703",
);
}

// y is a non-deterministic hint representing the cube root of the input at a step.
#[derive(Clone, Debug)]
struct CubeRootCheckingCircuit<F: PrimeField> {
y: Option<F>,
}

impl<F> StepCircuit<F> for CubeRootCheckingCircuit<F>
where
F: PrimeField,
{
fn arity(&self) -> usize {
1
}

fn circuit_index(&self) -> usize {
0
}

fn synthesize<CS: ConstraintSystem<F>>(
&self,
cs: &mut CS,
_pc: Option<&AllocatedNum<F>>,
z: &[AllocatedNum<F>],
) -> Result<(Option<AllocatedNum<F>>, Vec<AllocatedNum<F>>), SynthesisError> {
let x = &z[0];

// we allocate a variable and set it to the provided non-deterministic hint.
let y = AllocatedNum::alloc(cs.namespace(|| "y"), || {
self.y.ok_or(SynthesisError::AssignmentMissing)
})?;

// We now check if y = x^{1/3} by checking if y^3 = x
let y_sq = y.square(cs.namespace(|| "y_sq"))?;
let y_cube = y_sq.mul(cs.namespace(|| "y_cube"), &y)?;

cs.enforce(
|| "y^3 = x",
|lc| lc + y_cube.get_variable(),
|lc| lc + CS::one(),
|lc| lc + x.get_variable(),
);

let next_pc = alloc_const(&mut cs.namespace(|| "next_pc"), F::ONE)?;

Ok((Some(next_pc), vec![y]))
}
}

// y is a non-deterministic hint representing the fifth root of the input at a step.
#[derive(Clone, Debug)]
struct FifthRootCheckingCircuit<F: PrimeField> {
y: Option<F>,
}

impl<F> StepCircuit<F> for FifthRootCheckingCircuit<F>
where
F: PrimeField,
{
fn arity(&self) -> usize {
1
}

fn circuit_index(&self) -> usize {
1
}

fn synthesize<CS: ConstraintSystem<F>>(
&self,
cs: &mut CS,
_pc: Option<&AllocatedNum<F>>,
z: &[AllocatedNum<F>],
) -> Result<(Option<AllocatedNum<F>>, Vec<AllocatedNum<F>>), SynthesisError> {
let x = &z[0];

// we allocate a variable and set it to the provided non-deterministic hint.
let y = AllocatedNum::alloc(cs.namespace(|| "y"), || {
self.y.ok_or(SynthesisError::AssignmentMissing)
})?;

// We now check if y = x^{1/5} by checking if y^5 = x
let y_sq = y.square(cs.namespace(|| "y_sq"))?;
let y_quad = y_sq.square(cs.namespace(|| "y_quad"))?;
let y_pow_5 = y_quad.mul(cs.namespace(|| "y_fifth"), &y)?;

cs.enforce(
|| "y^5 = x",
|lc| lc + y_pow_5.get_variable(),
|lc| lc + CS::one(),
|lc| lc + x.get_variable(),
);

let next_pc = alloc_const(&mut cs.namespace(|| "next_pc"), F::ZERO)?;

Ok((Some(next_pc), vec![y]))
}
}

#[derive(Clone, Debug)]
enum RootCheckingCircuit<F: PrimeField> {
Cube(CubeRootCheckingCircuit<F>),
Fifth(FifthRootCheckingCircuit<F>),
}

impl<F: PrimeField> RootCheckingCircuit<F> {
fn new(num_steps: usize) -> (Vec<F>, Vec<Self>) {
let mut powers = Vec::new();
let rng = &mut rand::rngs::OsRng;
let mut seed = F::random(rng);

for i in 0..num_steps + 1 {
let seed_sq = seed.clone().square();
// Cube-root and fifth-root circuits alternate. We compute the hints backward, so the calculations appear to be
// associated with the 'wrong' circuit. The final circuit is discarded, and only the final seed is used (as z_0).
powers.push(if i % 2 == num_steps % 2 {
seed *= seed_sq;
Self::Fifth(FifthRootCheckingCircuit { y: Some(seed) })
} else {
seed *= seed_sq.clone().square();
Self::Cube(CubeRootCheckingCircuit { y: Some(seed) })
})
}

// reverse the powers to get roots
let roots = powers.into_iter().rev().collect::<Vec<Self>>();
(vec![roots[0].get_y().unwrap()], roots[1..].to_vec())
}

fn get_y(&self) -> Option<F> {
match self {
Self::Fifth(x) => x.y,
Self::Cube(x) => x.y,
}
}
}

impl<F> StepCircuit<F> for RootCheckingCircuit<F>
where
F: PrimeField,
{
fn arity(&self) -> usize {
1
}

fn circuit_index(&self) -> usize {
match self {
Self::Cube(x) => x.circuit_index(),
Self::Fifth(x) => x.circuit_index(),
}
}

fn synthesize<CS: ConstraintSystem<F>>(
&self,
cs: &mut CS,
pc: Option<&AllocatedNum<F>>,
z: &[AllocatedNum<F>],
) -> Result<(Option<AllocatedNum<F>>, Vec<AllocatedNum<F>>), SynthesisError> {
match self {
Self::Cube(c) => c.synthesize(cs, pc, z),
Self::Fifth(c) => c.synthesize(cs, pc, z),
}
}
}

impl<G1, G2>
NonUniformCircuit<G1, G2, RootCheckingCircuit<G1::Scalar>, TrivialSecondaryCircuit<G1::Base>>
for RootCheckingCircuit<G1::Scalar>
where
G1: Group<Base = <G2 as Group>::Scalar>,
G2: Group<Base = <G1 as Group>::Scalar>,
{
fn num_circuits(&self) -> usize {
2
}

fn primary_circuit(&self, circuit_index: usize) -> Self {
match circuit_index {
0 => Self::Cube(CubeRootCheckingCircuit { y: None }),
1 => Self::Fifth(FifthRootCheckingCircuit { y: None }),
_ => unreachable!(),
}
}

fn secondary_circuit(&self) -> TrivialSecondaryCircuit<G1::Base> {
TrivialSecondaryCircuit::<G1::Base>::default()
}
}

fn test_nivc_nondet_with<G1, G2>()
where
G1: Group<Base = <G2 as Group>::Scalar>,
G2: Group<Base = <G1 as Group>::Scalar>,
// this is due to the reliance on Abomonation
<<G1 as Group>::Scalar as PrimeField>::Repr: Abomonation,
<<G2 as Group>::Scalar as PrimeField>::Repr: Abomonation,
{
let circuit_secondary = TrivialSecondaryCircuit::default();

let num_steps = 3;

// produce non-deterministic hint
let (z0_primary, roots) = RootCheckingCircuit::new(num_steps);
assert_eq!(num_steps, roots.len());
let z0_secondary = vec![<G2 as Group>::Scalar::ZERO];

// produce public parameters
let pp = PublicParams::<
G1,
G2,
RootCheckingCircuit<<G1 as Group>::Scalar>,
TrivialSecondaryCircuit<<G2 as Group>::Scalar>,
>::new(&roots[0]);
// produce a recursive SNARK

let circuit_primary = &roots[0];
let mut recursive_snark = RecursiveSNARK::<G1, G2>::iter_base_step(
&pp,
circuit_primary.circuit_index(),
circuit_primary,
&circuit_secondary,
Some(G1::Scalar::from(circuit_primary.circuit_index() as u64)),
circuit_primary.circuit_index(),
2,
&z0_primary,
&z0_secondary,
)
.map_err(|err| {
print_constraints_name_on_error_index(
&err,
&pp,
circuit_primary,
&circuit_secondary,
<RootCheckingCircuit<G1::Scalar> as NonUniformCircuit<
G1,
G2,
RootCheckingCircuit<G1::Scalar>,
TrivialSecondaryCircuit<G1::Base>,
>>::num_circuits(circuit_primary),
)
})
.unwrap();

for circuit_primary in roots.iter().take(num_steps) {
let res = recursive_snark.prove_step(
&pp,
circuit_primary.circuit_index(),
circuit_primary,
&circuit_secondary,
);
assert!(res
.map_err(|err| {
print_constraints_name_on_error_index(
&err,
&pp,
circuit_primary,
&circuit_secondary,
<RootCheckingCircuit<G1::Scalar> as NonUniformCircuit<
G1,
G2,
RootCheckingCircuit<G1::Scalar>,
TrivialSecondaryCircuit<G1::Base>,
>>::num_circuits(circuit_primary),
)
})
.is_ok());

// verify the recursive SNARK
let res = recursive_snark
.verify(&pp, 0, &z0_primary, &z0_secondary)
.map_err(|err| {
print_constraints_name_on_error_index(
&err,
&pp,
circuit_primary,
&circuit_secondary,
<RootCheckingCircuit<G1::Scalar> as NonUniformCircuit<
G1,
G2,
RootCheckingCircuit<G1::Scalar>,
TrivialSecondaryCircuit<G1::Base>,
>>::num_circuits(circuit_primary),
)
});
assert!(res.is_ok());
}
}

#[test]
fn test_nivc_nondet() {
type G1 = pasta_curves::pallas::Point;
type G2 = pasta_curves::vesta::Point;

test_nivc_nondet_with::<G1, G2>();
test_nivc_nondet_with::<bn256::Point, grumpkin::Point>();
test_nivc_nondet_with::<secp256k1::Point, secq256k1::Point>();
}
12 changes: 9 additions & 3 deletions src/traits/circuit_supernova.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,7 @@ pub trait StepCircuit<F: PrimeField>: Send + Sync + Clone {
fn arity(&self) -> usize;

/// Return this `StepCircuit`'s assigned index, for use when enforcing the program counter.
fn circuit_index(&self) -> usize {
0
}
fn circuit_index(&self) -> usize;

/// Sythesize the circuit for a computation step and return variable
/// that corresponds to the output of the step `pc_{i+1}` and `z_{i+1}`
Expand Down Expand Up @@ -70,6 +68,10 @@ where
1
}

fn circuit_index(&self) -> usize {
0
}

fn synthesize<CS: ConstraintSystem<F>>(
&self,
_cs: &mut CS,
Expand All @@ -96,6 +98,10 @@ where
1
}

fn circuit_index(&self) -> usize {
0
}

fn synthesize<CS: ConstraintSystem<F>>(
&self,
_cs: &mut CS,
Expand Down

0 comments on commit 16cfdff

Please sign in to comment.