diff --git a/src/circuit.rs b/src/circuit.rs index d06ed8b..7b20ad6 100644 --- a/src/circuit.rs +++ b/src/circuit.rs @@ -12,7 +12,9 @@ use super::{ gadgets::{ ecc::AllocatedPoint, r1cs::{AllocatedR1CSInstance, AllocatedRelaxedR1CSInstance}, - utils::{alloc_num_equals, alloc_zero, conditionally_select, le_bits_to_num}, + utils::{ + alloc_num_equals, alloc_scalar_as_base, alloc_zero, conditionally_select, le_bits_to_num, + }, }, poseidon::{NovaPoseidonConstants, PoseidonROGadget}, r1cs::{R1CSInstance, RelaxedR1CSInstance}, @@ -32,26 +34,29 @@ use ff::Field; pub struct NIFSVerifierCircuitParams { limb_width: usize, n_limbs: usize, + is_primary_circuit: bool, // A boolean indicating if this is the primary circuit } impl NIFSVerifierCircuitParams { #[allow(dead_code)] - pub fn new(limb_width: usize, n_limbs: usize) -> Self { + pub fn new(limb_width: usize, n_limbs: usize, is_primary_circuit: bool) -> Self { Self { limb_width, n_limbs, + is_primary_circuit, } } } +#[derive(Debug)] pub struct NIFSVerifierCircuitInputs { - params: G::Base, // Hash(Shape of u2, Gens for u2). Needed for computing the challenge. + params: G::Scalar, // Hash(Shape of u2, Gens for u2). Needed for computing the challenge. i: G::Base, z0: G::Base, - zi: G::Base, - U: RelaxedR1CSInstance, - u: R1CSInstance, - T: Commitment, + zi: Option, + U: Option>, + u: Option>, + T: Option>, } impl NIFSVerifierCircuitInputs @@ -61,13 +66,13 @@ where /// Create new inputs/witness for the verification circuit #[allow(dead_code, clippy::too_many_arguments)] pub fn new( - params: G::Base, + params: G::Scalar, i: G::Base, z0: G::Base, - zi: G::Base, - U: RelaxedR1CSInstance, - u: R1CSInstance, - T: Commitment, + zi: Option, + U: Option>, + u: Option>, + T: Option>, ) -> Self { Self { params, @@ -131,46 +136,46 @@ where SynthesisError, > { // Allocate the params - let params = AllocatedNum::alloc(cs.namespace(|| "params"), || Ok(self.inputs.get()?.params))?; + let params = alloc_scalar_as_base::( + cs.namespace(|| "params"), + self.inputs.get().map_or(None, |inputs| Some(inputs.params)), + )?; // Allocate i let i = AllocatedNum::alloc(cs.namespace(|| "i"), || Ok(self.inputs.get()?.i))?; - // Allocate z0 let z_0 = AllocatedNum::alloc(cs.namespace(|| "z0"), || Ok(self.inputs.get()?.z0))?; - - // Allocate zi - let z_i = AllocatedNum::alloc(cs.namespace(|| "zi"), || Ok(self.inputs.get()?.zi))?; - + // Allocate zi. If inputs.zi is not provided (base case) allocate default value 0 + let z_i = AllocatedNum::alloc(cs.namespace(|| "zi"), || { + Ok(self.inputs.get()?.zi.unwrap_or_else(G::Base::zero)) + })?; // Allocate the running instance let U: AllocatedRelaxedR1CSInstance = AllocatedRelaxedR1CSInstance::alloc( cs.namespace(|| "Allocate U"), - self - .inputs - .get() - .map_or(None, |inputs| Some(inputs.U.clone())), + self.inputs.get().map_or(None, |inputs| { + inputs.U.get().map_or(None, |U| Some(U.clone())) + }), self.params.limb_width, self.params.n_limbs, )?; - // Allocate the instance to be folded in let u = AllocatedR1CSInstance::alloc( cs.namespace(|| "allocate instance u to fold"), - self - .inputs - .get() - .map_or(None, |inputs| Some(inputs.u.clone())), + self.inputs.get().map_or(None, |inputs| { + inputs.u.get().map_or(None, |u| Some(u.clone())) + }), )?; // Allocate T let T = AllocatedPoint::alloc( cs.namespace(|| "allocate T"), - self - .inputs - .get() - .map_or(None, |inputs| Some(inputs.T.comm.to_coordinates())), + self.inputs.get().map_or(None, |inputs| { + inputs + .T + .get() + .map_or(None, |T| Some(T.comm.to_coordinates())) + }), )?; - Ok((params, i, z_0, z_i, U, u, T)) } @@ -178,12 +183,24 @@ where fn synthesize_base_case::Base>>( &self, mut cs: CS, + u: AllocatedR1CSInstance, ) -> Result, SynthesisError> { - let U_default: AllocatedRelaxedR1CSInstance = AllocatedRelaxedR1CSInstance::default( - cs.namespace(|| "Allocate U_default"), - self.params.limb_width, - self.params.n_limbs, - )?; + let U_default: AllocatedRelaxedR1CSInstance = if self.params.is_primary_circuit { + // The primary circuit just returns the default R1CS instance + AllocatedRelaxedR1CSInstance::default( + cs.namespace(|| "Allocate U_default"), + self.params.limb_width, + self.params.n_limbs, + )? + } else { + // The secondary circuit returns the incoming R1CS instance + AllocatedRelaxedR1CSInstance::from_r1cs_instance( + cs.namespace(|| "Allocate U_default"), + u, + self.params.limb_width, + self.params.n_limbs, + )? + }; Ok(U_default) } @@ -250,7 +267,7 @@ where let is_base_case = alloc_num_equals(cs.namespace(|| "Check if base case"), &i.clone(), &zero)?; //TODO: maybe optimize this? // Synthesize the circuit for the base case and get the new running instance - let Unew_base = self.synthesize_base_case(cs.namespace(|| "base case"))?; + let Unew_base = self.synthesize_base_case(cs.namespace(|| "base case"), u.clone())?; // Synthesize the circuit for the non-base case and get the new running // instance along with a boolean indicating if all checks have passed @@ -336,7 +353,6 @@ mod tests { use crate::constants::{BN_LIMB_WIDTH, BN_N_LIMBS}; use crate::{ bellperson::r1cs::{NovaShape, NovaWitness}, - commitments::CommitTrait, traits::HashFuncConstantsTrait, }; use ff::PrimeField; @@ -361,22 +377,24 @@ mod tests { #[test] fn test_verification_circuit() { - // We experiment with 8 limbs of 32 bits each - let params = NIFSVerifierCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS); - // The first circuit that verifies G2 + // In the following we use 1 to refer to the primary, and 2 to refer to the secondary circuit + let params1 = NIFSVerifierCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS, true); + let params2 = NIFSVerifierCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS, false); let poseidon_constants1: NovaPoseidonConstants<::Base> = NovaPoseidonConstants::new(); + let poseidon_constants2: NovaPoseidonConstants<::Base> = + NovaPoseidonConstants::new(); + + // Initialize the shape and gens for the primary let circuit1: NIFSVerifierCircuit::Base>> = NIFSVerifierCircuit::new( - params.clone(), + params1.clone(), None, TestCircuit { _p: Default::default(), }, poseidon_constants1.clone(), ); - - // First create the shape let mut cs: ShapeCS = ShapeCS::new(); let _ = circuit1.synthesize(&mut cs); let (shape1, gens1) = (cs.r1cs_shape(), cs.r1cs_gens()); @@ -385,19 +403,16 @@ mod tests { cs.num_constraints() ); - // The second circuit that verifies G1 - let poseidon_constants2: NovaPoseidonConstants<::Base> = - NovaPoseidonConstants::new(); + // Initialize the shape and gens for the secondary let circuit2: NIFSVerifierCircuit::Base>> = NIFSVerifierCircuit::new( - params.clone(), + params2.clone(), None, TestCircuit { _p: Default::default(), }, - poseidon_constants2, + poseidon_constants2.clone(), ); - // First create the shape let mut cs: ShapeCS = ShapeCS::new(); let _ = circuit2.synthesize(&mut cs); let (shape2, gens2) = (cs.r1cs_shape(), cs.r1cs_gens()); @@ -406,35 +421,56 @@ mod tests { cs.num_constraints() ); - let zero = <::Base as Field>::zero(); - let zero_fq = <::Scalar as Field>::zero(); - let T = vec![::Scalar::zero()].commit(&gens2.gens_E); - let w = vec![::Scalar::zero()].commit(&gens2.gens_E); - // Now get an assignment - let mut cs: SatisfyingAssignment = SatisfyingAssignment::new(); - let inputs: NIFSVerifierCircuitInputs = NIFSVerifierCircuitInputs::new( - <::Base as Field>::zero(), // TODO: provide real inputs - zero, // TODO: provide real inputs - zero, // TODO: provide real inputs - zero, // TODO: provide real inputs - RelaxedR1CSInstance::default(&gens2, &shape2), - R1CSInstance::new(&shape2, &w, &[zero_fq, zero_fq]).unwrap(), - T, // TODO: provide real inputs + // Execute the base case for the primary + let zero1 = <::Base as Field>::zero(); + let mut cs1: SatisfyingAssignment = SatisfyingAssignment::new(); + let inputs1: NIFSVerifierCircuitInputs = NIFSVerifierCircuitInputs::new( + shape2.get_digest(), + zero1, + zero1, // TODO: Provide real input for z0 + None, + None, + None, + None, ); - - let circuit: NIFSVerifierCircuit::Base>> = + let circuit1: NIFSVerifierCircuit::Base>> = NIFSVerifierCircuit::new( - params, - Some(inputs), + params1, + Some(inputs1), TestCircuit { _p: Default::default(), }, poseidon_constants1, ); - let _ = circuit.synthesize(&mut cs); - let (inst, witness) = cs.r1cs_instance_and_witness(&shape1, &gens1).unwrap(); - + let _ = circuit1.synthesize(&mut cs1); + let (inst1, witness1) = cs1.r1cs_instance_and_witness(&shape1, &gens1).unwrap(); // Make sure that this is satisfiable - assert!(shape1.is_sat(&gens1, &inst, &witness).is_ok()); + assert!(shape1.is_sat(&gens1, &inst1, &witness1).is_ok()); + + // Execute the base case for the secondary + let zero2 = <::Base as Field>::zero(); + let mut cs2: SatisfyingAssignment = SatisfyingAssignment::new(); + let inputs2: NIFSVerifierCircuitInputs = NIFSVerifierCircuitInputs::new( + shape1.get_digest(), + zero2, + zero2, + None, + None, + Some(inst1), + None, + ); + let circuit: NIFSVerifierCircuit::Base>> = + NIFSVerifierCircuit::new( + params2, + Some(inputs2), + TestCircuit { + _p: Default::default(), + }, + poseidon_constants2, + ); + let _ = circuit.synthesize(&mut cs2); + let (inst2, witness2) = cs2.r1cs_instance_and_witness(&shape2, &gens2).unwrap(); + // Make sure that it is satisfiable + assert!(shape2.is_sat(&gens2, &inst2, &witness2).is_ok()); } } diff --git a/src/gadgets/ecc.rs b/src/gadgets/ecc.rs index 9f2a488..3e10353 100644 --- a/src/gadgets/ecc.rs +++ b/src/gadgets/ecc.rs @@ -29,14 +29,19 @@ where Fp: PrimeField, { /// Allocates a new point on the curve using coordinates provided by `coords`. + /// If coords = None, it allocates the default infinity point pub fn alloc(mut cs: CS, coords: Option<(Fp, Fp, bool)>) -> Result where CS: ConstraintSystem, { - let x = AllocatedNum::alloc(cs.namespace(|| "x"), || Ok(coords.unwrap().0))?; - let y = AllocatedNum::alloc(cs.namespace(|| "y"), || Ok(coords.unwrap().1))?; + let x = AllocatedNum::alloc(cs.namespace(|| "x"), || { + Ok(coords.map_or(Fp::zero(), |c| c.0)) + })?; + let y = AllocatedNum::alloc(cs.namespace(|| "y"), || { + Ok(coords.map_or(Fp::zero(), |c| c.0)) + })?; let is_infinity = AllocatedNum::alloc(cs.namespace(|| "is_infinity"), || { - Ok(if coords.unwrap().2 { + Ok(if coords.map_or(true, |c| c.2) { Fp::one() } else { Fp::zero() diff --git a/src/gadgets/r1cs.rs b/src/gadgets/r1cs.rs index 7cab720..990121a 100644 --- a/src/gadgets/r1cs.rs +++ b/src/gadgets/r1cs.rs @@ -3,7 +3,7 @@ use crate::{ gadgets::{ ecc::AllocatedPoint, utils::{ - alloc_bignat_constant, alloc_scalar_as_base, conditionally_select, + alloc_bignat_constant, alloc_one, alloc_scalar_as_base, conditionally_select, conditionally_select_bignat, le_bits_to_num, }, }, @@ -114,16 +114,25 @@ where inst.get().map_or(None, |inst| Some(inst.u)), )?; + // Allocate X0 and X1. If the input instance is None, then allocate default values 0. let X0 = BigNat::alloc_from_nat( cs.namespace(|| "allocate X[0]"), - || Ok(f_to_nat(&inst.get()?.X[0])), + || { + Ok(f_to_nat( + &inst.clone().map_or(G::Scalar::zero(), |inst| inst.X[0]), + )) + }, limb_width, n_limbs, )?; let X1 = BigNat::alloc_from_nat( cs.namespace(|| "allocate X[1]"), - || Ok(f_to_nat(&inst.get()?.X[1])), + || { + Ok(f_to_nat( + &inst.clone().map_or(G::Scalar::zero(), |inst| inst.X[1]), + )) + }, limb_width, n_limbs, )?; @@ -160,6 +169,41 @@ where Ok(AllocatedRelaxedR1CSInstance { W, E, u, X0, X1 }) } + /// Allocates the R1CS Instance as a RelaxedR1CSInstance in the circuit. + /// E = 0, u = 1 + pub fn from_r1cs_instance::Base>>( + mut cs: CS, + inst: AllocatedR1CSInstance, + limb_width: usize, + n_limbs: usize, + ) -> Result { + let E = AllocatedPoint::default(cs.namespace(|| "allocate W"))?; + + let u = alloc_one(cs.namespace(|| "one"))?; + + let X0 = BigNat::from_num( + cs.namespace(|| "allocate X0 from relaxed r1cs"), + Num::from(inst.X0.clone()), + limb_width, + n_limbs, + )?; + + let X1 = BigNat::from_num( + cs.namespace(|| "allocate X1 from relaxed r1cs"), + Num::from(inst.X1.clone()), + limb_width, + n_limbs, + )?; + + Ok(AllocatedRelaxedR1CSInstance { + W: inst.W, + E, + u, + X0, + X1, + }) + } + /// Absorb the provided instance in the RO pub fn absorb_in_ro::Base>>( &self, diff --git a/src/gadgets/utils.rs b/src/gadgets/utils.rs index 7b28147..2034544 100644 --- a/src/gadgets/utils.rs +++ b/src/gadgets/utils.rs @@ -86,7 +86,7 @@ where CS: ConstraintSystem<::Base>, { AllocatedNum::alloc(cs.namespace(|| "allocate scalar as base"), || { - let input_bits = input.get()?.clone().to_le_bits(); + let input_bits = input.unwrap_or_else(G::Scalar::zero).clone().to_le_bits(); let mut mult = G::Base::one(); let mut val = G::Base::zero(); for bit in input_bits {