arnaucube/Nova
1
0
Fork 0
mirror of https://github.com/arnaucube/Nova.git synced 2026-01-11 16:41:28 +01:00
Code Issues Projects Releases Wiki Activity

Base case for second circuit (#60)

Browse Source 
* output the incoming instance as the running instance in one of the circuits

* Make some verifier circuit inputs optional (for base case)
This commit is contained in:
iontzialla
2022-05-14 10:56:57 -04:00
committed by GitHub
parent 3193d67bce
commit 9f7c12dbc5
4 changed files with 165 additions and 80 deletions
Download Patch File Download Diff File Expand all files Collapse all files

174
src/circuit.rs
View File

@@ -12,7 +12,9 @@ use super::{
gadgets::{ gadgets::{
ecc::AllocatedPoint, ecc::AllocatedPoint,
r1cs::{AllocatedR1CSInstance, AllocatedRelaxedR1CSInstance}, 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}, poseidon::{NovaPoseidonConstants, PoseidonROGadget},
r1cs::{R1CSInstance, RelaxedR1CSInstance}, r1cs::{R1CSInstance, RelaxedR1CSInstance},
@@ -32,26 +34,29 @@ use ff::Field;
pub struct NIFSVerifierCircuitParams { pub struct NIFSVerifierCircuitParams {
limb_width: usize, limb_width: usize,
n_limbs: usize, n_limbs: usize,
is_primary_circuit: bool, // A boolean indicating if this is the primary circuit
} }
impl NIFSVerifierCircuitParams { impl NIFSVerifierCircuitParams {
#[allow(dead_code)] #[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 { Self {
limb_width, limb_width,
n_limbs, n_limbs,
is_primary_circuit,
} }
} }
} }
#[derive(Debug)]
pub struct NIFSVerifierCircuitInputs<G: Group> { pub struct NIFSVerifierCircuitInputs<G: Group> {
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, i: G::Base,
z0: G::Base, z0: G::Base,
zi: G::Base, zi: Option<G::Base>,
U: RelaxedR1CSInstance<G>, U: Option<RelaxedR1CSInstance<G>>,
u: R1CSInstance<G>, u: Option<R1CSInstance<G>>,
T: Commitment<G>, T: Option<Commitment<G>>,
} }
impl<G> NIFSVerifierCircuitInputs<G> impl<G> NIFSVerifierCircuitInputs<G>
@@ -61,13 +66,13 @@ where
/// Create new inputs/witness for the verification circuit /// Create new inputs/witness for the verification circuit
#[allow(dead_code, clippy::too_many_arguments)] #[allow(dead_code, clippy::too_many_arguments)]
pub fn new( pub fn new(
params: G::Base, params: G::Scalar,
i: G::Base, i: G::Base,
z0: G::Base, z0: G::Base,
zi: G::Base, zi: Option<G::Base>,
U: RelaxedR1CSInstance<G>, U: Option<RelaxedR1CSInstance<G>>,
u: R1CSInstance<G>, u: Option<R1CSInstance<G>>,
T: Commitment<G>, T: Option<Commitment<G>>,
) -> Self { ) -> Self {
Self { Self {
params, params,
@@ -131,46 +136,46 @@ where
SynthesisError, SynthesisError,
> { > {
// Allocate the params // Allocate the params
let params = AllocatedNum::alloc(cs.namespace(|| "params"), || Ok(self.inputs.get()?.params))?; let params = alloc_scalar_as_base::<G, _>(
cs.namespace(|| "params"),
self.inputs.get().map_or(None, |inputs| Some(inputs.params)),
)?;
// Allocate i // Allocate i
let i = AllocatedNum::alloc(cs.namespace(|| "i"), || Ok(self.inputs.get()?.i))?; let i = AllocatedNum::alloc(cs.namespace(|| "i"), || Ok(self.inputs.get()?.i))?;
// Allocate z0 // Allocate z0
let z_0 = AllocatedNum::alloc(cs.namespace(|| "z0"), || Ok(self.inputs.get()?.z0))?; let z_0 = AllocatedNum::alloc(cs.namespace(|| "z0"), || Ok(self.inputs.get()?.z0))?;
// Allocate zi. If inputs.zi is not provided (base case) allocate default value 0
// Allocate zi let z_i = AllocatedNum::alloc(cs.namespace(|| "zi"), || {
let z_i = AllocatedNum::alloc(cs.namespace(|| "zi"), || Ok(self.inputs.get()?.zi))?; Ok(self.inputs.get()?.zi.unwrap_or_else(G::Base::zero))
})?;
// Allocate the running instance // Allocate the running instance
let U: AllocatedRelaxedR1CSInstance<G> = AllocatedRelaxedR1CSInstance::alloc( let U: AllocatedRelaxedR1CSInstance<G> = AllocatedRelaxedR1CSInstance::alloc(
cs.namespace(|| "Allocate U"), cs.namespace(|| "Allocate U"),
self self.inputs.get().map_or(None, |inputs| {
.inputs inputs.U.get().map_or(None, |U| Some(U.clone()))
.get() }),
.map_or(None, |inputs| Some(inputs.U.clone())),
self.params.limb_width, self.params.limb_width,
self.params.n_limbs, self.params.n_limbs,
)?; )?;
// Allocate the instance to be folded in // Allocate the instance to be folded in
let u = AllocatedR1CSInstance::alloc( let u = AllocatedR1CSInstance::alloc(
cs.namespace(|| "allocate instance u to fold"), cs.namespace(|| "allocate instance u to fold"),
self self.inputs.get().map_or(None, |inputs| {
.inputs inputs.u.get().map_or(None, |u| Some(u.clone()))
.get() }),
.map_or(None, |inputs| Some(inputs.u.clone())),
)?; )?;
// Allocate T // Allocate T
let T = AllocatedPoint::alloc( let T = AllocatedPoint::alloc(
cs.namespace(|| "allocate T"), cs.namespace(|| "allocate T"),
self self.inputs.get().map_or(None, |inputs| {
.inputs inputs
.T
.get() .get()
.map_or(None, |inputs| Some(inputs.T.comm.to_coordinates())), .map_or(None, |T| Some(T.comm.to_coordinates()))
}),
)?; )?;
Ok((params, i, z_0, z_i, U, u, T)) Ok((params, i, z_0, z_i, U, u, T))
} }
@@ -178,12 +183,24 @@ where
fn synthesize_base_case<CS: ConstraintSystem<<G as Group>::Base>>( fn synthesize_base_case<CS: ConstraintSystem<<G as Group>::Base>>(
&self, &self,
mut cs: CS, mut cs: CS,
u: AllocatedR1CSInstance<G>,
) -> Result<AllocatedRelaxedR1CSInstance<G>, SynthesisError> { ) -> Result<AllocatedRelaxedR1CSInstance<G>, SynthesisError> {
let U_default: AllocatedRelaxedR1CSInstance<G> = AllocatedRelaxedR1CSInstance::default( let U_default: AllocatedRelaxedR1CSInstance<G> = if self.params.is_primary_circuit {
// The primary circuit just returns the default R1CS instance
AllocatedRelaxedR1CSInstance::default(
cs.namespace(|| "Allocate U_default"), cs.namespace(|| "Allocate U_default"),
self.params.limb_width, self.params.limb_width,
self.params.n_limbs, 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) 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? 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 // 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 // Synthesize the circuit for the non-base case and get the new running
// instance along with a boolean indicating if all checks have passed // 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::constants::{BN_LIMB_WIDTH, BN_N_LIMBS};
use crate::{ use crate::{
bellperson::r1cs::{NovaShape, NovaWitness}, bellperson::r1cs::{NovaShape, NovaWitness},
commitments::CommitTrait,
traits::HashFuncConstantsTrait, traits::HashFuncConstantsTrait,
}; };
use ff::PrimeField; use ff::PrimeField;
@@ -361,22 +377,24 @@ mod tests {
#[test] #[test]
fn test_verification_circuit() { fn test_verification_circuit() {
// We experiment with 8 limbs of 32 bits each // In the following we use 1 to refer to the primary, and 2 to refer to the secondary circuit
let params = NIFSVerifierCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS); let params1 = NIFSVerifierCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS, true);
// The first circuit that verifies G2 let params2 = NIFSVerifierCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS, false);
let poseidon_constants1: NovaPoseidonConstants<<G2 as Group>::Base> = let poseidon_constants1: NovaPoseidonConstants<<G2 as Group>::Base> =
NovaPoseidonConstants::new(); NovaPoseidonConstants::new();
let poseidon_constants2: NovaPoseidonConstants<<G1 as Group>::Base> =
NovaPoseidonConstants::new();
// Initialize the shape and gens for the primary
let circuit1: NIFSVerifierCircuit<G2, TestCircuit<<G2 as Group>::Base>> = let circuit1: NIFSVerifierCircuit<G2, TestCircuit<<G2 as Group>::Base>> =
NIFSVerifierCircuit::new( NIFSVerifierCircuit::new(
params.clone(), params1.clone(),
None, None,
TestCircuit { TestCircuit {
_p: Default::default(), _p: Default::default(),
}, },
poseidon_constants1.clone(), poseidon_constants1.clone(),
); );
// First create the shape
let mut cs: ShapeCS<G1> = ShapeCS::new(); let mut cs: ShapeCS<G1> = ShapeCS::new();
let _ = circuit1.synthesize(&mut cs); let _ = circuit1.synthesize(&mut cs);
let (shape1, gens1) = (cs.r1cs_shape(), cs.r1cs_gens()); let (shape1, gens1) = (cs.r1cs_shape(), cs.r1cs_gens());
@@ -385,19 +403,16 @@ mod tests {
cs.num_constraints() cs.num_constraints()
); );
// The second circuit that verifies G1 // Initialize the shape and gens for the secondary
let poseidon_constants2: NovaPoseidonConstants<<G1 as Group>::Base> =
NovaPoseidonConstants::new();
let circuit2: NIFSVerifierCircuit<G1, TestCircuit<<G1 as Group>::Base>> = let circuit2: NIFSVerifierCircuit<G1, TestCircuit<<G1 as Group>::Base>> =
NIFSVerifierCircuit::new( NIFSVerifierCircuit::new(
params.clone(), params2.clone(),
None, None,
TestCircuit { TestCircuit {
_p: Default::default(), _p: Default::default(),
}, },
poseidon_constants2, poseidon_constants2.clone(),
); );
// First create the shape
let mut cs: ShapeCS<G2> = ShapeCS::new(); let mut cs: ShapeCS<G2> = ShapeCS::new();
let _ = circuit2.synthesize(&mut cs); let _ = circuit2.synthesize(&mut cs);
let (shape2, gens2) = (cs.r1cs_shape(), cs.r1cs_gens()); let (shape2, gens2) = (cs.r1cs_shape(), cs.r1cs_gens());
@@ -406,35 +421,56 @@ mod tests {
cs.num_constraints() cs.num_constraints()
); );
let zero = <<G2 as Group>::Base as Field>::zero(); // Execute the base case for the primary
let zero_fq = <<G2 as Group>::Scalar as Field>::zero(); let zero1 = <<G2 as Group>::Base as Field>::zero();
let T = vec![<G2 as Group>::Scalar::zero()].commit(&gens2.gens_E); let mut cs1: SatisfyingAssignment<G1> = SatisfyingAssignment::new();
let w = vec![<G2 as Group>::Scalar::zero()].commit(&gens2.gens_E); let inputs1: NIFSVerifierCircuitInputs<G2> = NIFSVerifierCircuitInputs::new(
// Now get an assignment shape2.get_digest(),
let mut cs: SatisfyingAssignment<G1> = SatisfyingAssignment::new(); zero1,
let inputs: NIFSVerifierCircuitInputs<G2> = NIFSVerifierCircuitInputs::new( zero1, // TODO: Provide real input for z0
<<G2 as Group>::Base as Field>::zero(), // TODO: provide real inputs None,
zero, // TODO: provide real inputs None,
zero, // TODO: provide real inputs None,
zero, // TODO: provide real inputs None,
RelaxedR1CSInstance::default(&gens2, &shape2),
R1CSInstance::new(&shape2, &w, &[zero_fq, zero_fq]).unwrap(),
T, // TODO: provide real inputs
); );
let circuit1: NIFSVerifierCircuit<G2, TestCircuit<<G2 as Group>::Base>> =
let circuit: NIFSVerifierCircuit<G2, TestCircuit<<G2 as Group>::Base>> =
NIFSVerifierCircuit::new( NIFSVerifierCircuit::new(
params, params1,
Some(inputs), Some(inputs1),
TestCircuit { TestCircuit {
_p: Default::default(), _p: Default::default(),
}, },
poseidon_constants1, poseidon_constants1,
); );
let _ = circuit.synthesize(&mut cs); let _ = circuit1.synthesize(&mut cs1);
let (inst, witness) = cs.r1cs_instance_and_witness(&shape1, &gens1).unwrap(); let (inst1, witness1) = cs1.r1cs_instance_and_witness(&shape1, &gens1).unwrap();
// Make sure that this is satisfiable // 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 = <<G1 as Group>::Base as Field>::zero();
let mut cs2: SatisfyingAssignment<G2> = SatisfyingAssignment::new();
let inputs2: NIFSVerifierCircuitInputs<G1> = NIFSVerifierCircuitInputs::new(
shape1.get_digest(),
zero2,
zero2,
None,
None,
Some(inst1),
None,
);
let circuit: NIFSVerifierCircuit<G1, TestCircuit<<G1 as Group>::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());
} }
} }

11
src/gadgets/ecc.rs
View File

@@ -29,14 +29,19 @@ where
Fp: PrimeField, Fp: PrimeField,
{ {
/// Allocates a new point on the curve using coordinates provided by `coords`. /// Allocates a new point on the curve using coordinates provided by `coords`.
/// If coords = None, it allocates the default infinity point
pub fn alloc<CS>(mut cs: CS, coords: Option<(Fp, Fp, bool)>) -> Result<Self, SynthesisError> pub fn alloc<CS>(mut cs: CS, coords: Option<(Fp, Fp, bool)>) -> Result<Self, SynthesisError>
where where
CS: ConstraintSystem<Fp>, CS: ConstraintSystem<Fp>,
{ {
let x = AllocatedNum::alloc(cs.namespace(|| "x"), || Ok(coords.unwrap().0))?; let x = AllocatedNum::alloc(cs.namespace(|| "x"), || {
let y = AllocatedNum::alloc(cs.namespace(|| "y"), || Ok(coords.unwrap().1))?; 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"), || { 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() Fp::one()
} else { } else {
Fp::zero() Fp::zero()

50
src/gadgets/r1cs.rs
View File

@@ -3,7 +3,7 @@ use crate::{
gadgets::{ gadgets::{
ecc::AllocatedPoint, ecc::AllocatedPoint,
utils::{ 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, conditionally_select_bignat, le_bits_to_num,
}, },
}, },
@@ -114,16 +114,25 @@ where
inst.get().map_or(None, |inst| Some(inst.u)), 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( let X0 = BigNat::alloc_from_nat(
cs.namespace(|| "allocate X[0]"), 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, limb_width,
n_limbs, n_limbs,
)?; )?;
let X1 = BigNat::alloc_from_nat( let X1 = BigNat::alloc_from_nat(
cs.namespace(|| "allocate X[1]"), 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, limb_width,
n_limbs, n_limbs,
)?; )?;
@@ -160,6 +169,41 @@ where
Ok(AllocatedRelaxedR1CSInstance { W, E, u, X0, X1 }) 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<CS: ConstraintSystem<<G as Group>::Base>>(
mut cs: CS,
inst: AllocatedR1CSInstance<G>,
limb_width: usize,
n_limbs: usize,
) -> Result<Self, SynthesisError> {
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 /// Absorb the provided instance in the RO
pub fn absorb_in_ro<CS: ConstraintSystem<<G as Group>::Base>>( pub fn absorb_in_ro<CS: ConstraintSystem<<G as Group>::Base>>(
&self, &self,

2
src/gadgets/utils.rs
View File

@@ -86,7 +86,7 @@ where
CS: ConstraintSystem<<G as Group>::Base>, CS: ConstraintSystem<<G as Group>::Base>,
{ {
AllocatedNum::alloc(cs.namespace(|| "allocate scalar as 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 mult = G::Base::one();
let mut val = G::Base::zero(); let mut val = G::Base::zero();
for bit in input_bits { for bit in input_bits {