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

Add non-deterministic ivc test. #92

Merged
merged 1 commit into from
Nov 2, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
Loading