Nova/src/circuit.rs
src/circuit.rsRaw
1//! There are two Verification Circuits. The primary and the secondary.
2//! Each of them is over a Pasta curve but
3//! only the primary executes the next step of the computation.
4//! TODO: The base case is different for the primary and the secondary.
5//! We have two running instances. Each circuit takes as input 2 hashes: one for each
6//! of the running instances. Each of these hashes is
7//! H(params = H(shape, gens), i, z0, zi, U). Each circuit folds the last invocation of
8//! the other into the running instance
9
10use super::{
11 commitments::Commitment,
12 gadgets::{
13 ecc::AllocatedPoint,
14 r1cs::{AllocatedR1CSInstance, AllocatedRelaxedR1CSInstance},
15 utils::{
16 alloc_num_equals, alloc_scalar_as_base, alloc_zero, conditionally_select, le_bits_to_num,
17 },
18 },
19 poseidon::{PoseidonROGadget, ROConstantsCircuit},
20 r1cs::{R1CSInstance, RelaxedR1CSInstance},
21 traits::{Group, StepCircuit},
22};
23use bellperson::{
24 gadgets::{
25 boolean::{AllocatedBit, Boolean},
26 num::AllocatedNum,
27 Assignment,
28 },
29 Circuit, ConstraintSystem, SynthesisError,
30};
31use ff::Field;
32
33#[derive(Debug, Clone)]
34pub struct NIFSVerifierCircuitParams {
35 limb_width: usize,
36 n_limbs: usize,
37 is_primary_circuit: bool, // A boolean indicating if this is the primary circuit
38}
39
40impl NIFSVerifierCircuitParams {
41 #[allow(dead_code)]
42 pub fn new(limb_width: usize, n_limbs: usize, is_primary_circuit: bool) -> Self {
43 Self {
44 limb_width,
45 n_limbs,
46 is_primary_circuit,
47 }
48 }
49}
50
51#[derive(Debug)]
52pub struct NIFSVerifierCircuitInputs<G: Group> {
53 params: G::Scalar, // Hash(Shape of u2, Gens for u2). Needed for computing the challenge.
54 i: G::Base,
55 z0: G::Base,
56 zi: Option<G::Base>,
57 U: Option<RelaxedR1CSInstance<G>>,
58 u: Option<R1CSInstance<G>>,
59 T: Option<Commitment<G>>,
60}
61
62impl<G> NIFSVerifierCircuitInputs<G>
63where
64 G: Group,
65{
66 /// Create new inputs/witness for the verification circuit
67 #[allow(dead_code, clippy::too_many_arguments)]
68 pub fn new(
69 params: G::Scalar,
70 i: G::Base,
71 z0: G::Base,
72 zi: Option<G::Base>,
73 U: Option<RelaxedR1CSInstance<G>>,
74 u: Option<R1CSInstance<G>>,
75 T: Option<Commitment<G>>,
76 ) -> Self {
77 Self {
78 params,
79 i,
80 z0,
81 zi,
82 U,
83 u,
84 T,
85 }
86 }
87}
88
89/// Circuit that encodes only the folding verifier
90pub struct NIFSVerifierCircuit<G, SC>
91where
92 G: Group,
93 SC: StepCircuit<G::Base>,
94{
95 params: NIFSVerifierCircuitParams,
96 ro_consts: ROConstantsCircuit<G::Base>,
97 inputs: Option<NIFSVerifierCircuitInputs<G>>,
98 step_circuit: SC, // The function that is applied for each step
99}
100
101impl<G, SC> NIFSVerifierCircuit<G, SC>
102where
103 G: Group,
104 SC: StepCircuit<G::Base>,
105{
106 /// Create a new verification circuit for the input relaxed r1cs instances
107 #[allow(dead_code)]
108 pub fn new(
109 params: NIFSVerifierCircuitParams,
110 inputs: Option<NIFSVerifierCircuitInputs<G>>,
111 step_circuit: SC,
112 ro_consts: ROConstantsCircuit<G::Base>,
113 ) -> Self {
114 Self {
115 params,
116 inputs,
117 step_circuit,
118 ro_consts,
119 }
120 }
121
122 /// Allocate all witnesses and return
123 fn alloc_witness<CS: ConstraintSystem<<G as Group>::Base>>(
124 &self,
125 mut cs: CS,
126 ) -> Result<
127 (
128 AllocatedNum<G::Base>,
129 AllocatedNum<G::Base>,
130 AllocatedNum<G::Base>,
131 AllocatedNum<G::Base>,
132 AllocatedRelaxedR1CSInstance<G>,
133 AllocatedR1CSInstance<G>,
134 AllocatedPoint<G::Base>,
135 ),
136 SynthesisError,
137 > {
138 // Allocate the params
139 let params = alloc_scalar_as_base::<G, _>(
140 cs.namespace(|| "params"),
141 self.inputs.get().map_or(None, |inputs| Some(inputs.params)),
142 )?;
143
144 // Allocate i
145 let i = AllocatedNum::alloc(cs.namespace(|| "i"), || Ok(self.inputs.get()?.i))?;
146 // Allocate z0
147 let z_0 = AllocatedNum::alloc(cs.namespace(|| "z0"), || Ok(self.inputs.get()?.z0))?;
148 // Allocate zi. If inputs.zi is not provided (base case) allocate default value 0
149 let z_i = AllocatedNum::alloc(cs.namespace(|| "zi"), || {
150 Ok(self.inputs.get()?.zi.unwrap_or_else(G::Base::zero))
151 })?;
152 // Allocate the running instance
153 let U: AllocatedRelaxedR1CSInstance<G> = AllocatedRelaxedR1CSInstance::alloc(
154 cs.namespace(|| "Allocate U"),
155 self.inputs.get().map_or(None, |inputs| {
156 inputs.U.get().map_or(None, |U| Some(U.clone()))
157 }),
158 self.params.limb_width,
159 self.params.n_limbs,
160 )?;
161 // Allocate the instance to be folded in
162 let u = AllocatedR1CSInstance::alloc(
163 cs.namespace(|| "allocate instance u to fold"),
164 self.inputs.get().map_or(None, |inputs| {
165 inputs.u.get().map_or(None, |u| Some(u.clone()))
166 }),
167 )?;
168
169 // Allocate T
170 let T = AllocatedPoint::alloc(
171 cs.namespace(|| "allocate T"),
172 self.inputs.get().map_or(None, |inputs| {
173 inputs
174 .T
175 .get()
176 .map_or(None, |T| Some(T.comm.to_coordinates()))
177 }),
178 )?;
179 Ok((params, i, z_0, z_i, U, u, T))
180 }
181
182 /// Synthesizes base case and returns the new relaxed R1CSInstance
183 fn synthesize_base_case<CS: ConstraintSystem<<G as Group>::Base>>(
184 &self,
185 mut cs: CS,
186 u: AllocatedR1CSInstance<G>,
187 ) -> Result<AllocatedRelaxedR1CSInstance<G>, SynthesisError> {
188 let U_default: AllocatedRelaxedR1CSInstance<G> = if self.params.is_primary_circuit {
189 // The primary circuit just returns the default R1CS instance
190 AllocatedRelaxedR1CSInstance::default(
191 cs.namespace(|| "Allocate U_default"),
192 self.params.limb_width,
193 self.params.n_limbs,
194 )?
195 } else {
196 // The secondary circuit returns the incoming R1CS instance
197 AllocatedRelaxedR1CSInstance::from_r1cs_instance(
198 cs.namespace(|| "Allocate U_default"),
199 u,
200 self.params.limb_width,
201 self.params.n_limbs,
202 )?
203 };
204 Ok(U_default)
205 }
206
207 /// Synthesizes non base case and returns the new relaxed R1CSInstance
208 /// And a boolean indicating if all checks pass
209 #[allow(clippy::too_many_arguments)]
210 fn synthesize_non_base_case<CS: ConstraintSystem<<G as Group>::Base>>(
211 &self,
212 mut cs: CS,
213 params: AllocatedNum<G::Base>,
214 i: AllocatedNum<G::Base>,
215 z_0: AllocatedNum<G::Base>,
216 z_i: AllocatedNum<G::Base>,
217 U: AllocatedRelaxedR1CSInstance<G>,
218 u: AllocatedR1CSInstance<G>,
219 T: AllocatedPoint<G::Base>,
220 ) -> Result<(AllocatedRelaxedR1CSInstance<G>, AllocatedBit), SynthesisError> {
221 // Check that u.x[0] = Hash(params, U, i, z0, zi)
222 let mut ro: PoseidonROGadget<G::Base> = PoseidonROGadget::new(self.ro_consts.clone());
223 ro.absorb(params.clone());
224 ro.absorb(i);
225 ro.absorb(z_0);
226 ro.absorb(z_i);
227 let _ = U.absorb_in_ro(cs.namespace(|| "absorb U"), &mut ro)?;
228
229 let hash_bits = ro.get_hash(cs.namespace(|| "Input hash"))?;
230 let hash = le_bits_to_num(cs.namespace(|| "bits to hash"), hash_bits)?;
231 let check_pass = alloc_num_equals(
232 cs.namespace(|| "check consistency of u.X[0] with H(params, U, i, z0, zi)"),
233 &u.X0,
234 &hash,
235 )?;
236
237 // Run NIFS Verifier
238 let U_fold = U.fold_with_r1cs(
239 cs.namespace(|| "compute fold of U and u"),
240 params,
241 u,
242 T,
243 self.ro_consts.clone(),
244 self.params.limb_width,
245 self.params.n_limbs,
246 )?;
247
248 Ok((U_fold, check_pass))
249 }
250}
251
252impl<G, SC> Circuit<<G as Group>::Base> for NIFSVerifierCircuit<G, SC>
253where
254 G: Group,
255 SC: StepCircuit<G::Base>,
256{
257 fn synthesize<CS: ConstraintSystem<<G as Group>::Base>>(
258 self,
259 cs: &mut CS,
260 ) -> Result<(), SynthesisError> {
261 // Allocate all witnesses
262 let (params, i, z_0, z_i, U, u, T) =
263 self.alloc_witness(cs.namespace(|| "allocate the circuit witness"))?;
264
265 // Compute variable indicating if this is the base case
266 let zero = alloc_zero(cs.namespace(|| "zero"))?;
267 let is_base_case = alloc_num_equals(cs.namespace(|| "Check if base case"), &i.clone(), &zero)?; //TODO: maybe optimize this?
268
269 // Synthesize the circuit for the base case and get the new running instance
270 let Unew_base = self.synthesize_base_case(cs.namespace(|| "base case"), u.clone())?;
271
272 // Synthesize the circuit for the non-base case and get the new running
273 // instance along with a boolean indicating if all checks have passed
274 let (Unew_non_base, check_non_base_pass) = self.synthesize_non_base_case(
275 cs.namespace(|| "synthesize non base case"),
276 params.clone(),
277 i.clone(),
278 z_0.clone(),
279 z_i.clone(),
280 U,
281 u.clone(),
282 T,
283 )?;
284
285 // Either check_non_base_pass=true or we are in the base case
286 let should_be_false = AllocatedBit::nor(
287 cs.namespace(|| "check_non_base_pass nor base_case"),
288 &check_non_base_pass,
289 &is_base_case,
290 )?;
291 cs.enforce(
292 || "check_non_base_pass nor base_case = false",
293 |lc| lc + should_be_false.get_variable(),
294 |lc| lc + CS::one(),
295 |lc| lc,
296 );
297
298 // Compute the U_new
299 let Unew = Unew_base.conditionally_select(
300 cs.namespace(|| "compute U_new"),
301 Unew_non_base,
302 &Boolean::from(is_base_case.clone()),
303 )?;
304
305 // Compute i + 1
306 let i_new = AllocatedNum::alloc(cs.namespace(|| "i + 1"), || {
307 Ok(*i.get_value().get()? + G::Base::one())
308 })?;
309 cs.enforce(
310 || "check i + 1",
311 |lc| lc,
312 |lc| lc,
313 |lc| lc + i_new.get_variable() - CS::one() - i.get_variable(),
314 );
315
316 // Compute z_{i+1}
317 let z_input = conditionally_select(
318 cs.namespace(|| "select input to F"),
319 &z_0,
320 &z_i,
321 &Boolean::from(is_base_case),
322 )?;
323 let z_next = self
324 .step_circuit
325 .synthesize(&mut cs.namespace(|| "F"), z_input)?;
326
327 // Compute the new hash H(params, Unew, i+1, z0, z_{i+1})
328 let mut ro: PoseidonROGadget<G::Base> = PoseidonROGadget::new(self.ro_consts);
329 ro.absorb(params);
330 ro.absorb(i_new.clone());
331 ro.absorb(z_0);
332 ro.absorb(z_next);
333 let _ = Unew.absorb_in_ro(cs.namespace(|| "absorb U_new"), &mut ro)?;
334 let hash_bits = ro.get_hash(cs.namespace(|| "output hash bits"))?;
335 let hash = le_bits_to_num(cs.namespace(|| "convert hash to num"), hash_bits)?;
336
337 // Outputs the computed hash and u.X[1] that corresponds to the hash of the other circuit
338 let _ = u
339 .X1
340 .inputize(cs.namespace(|| "Output unmodified hash of the other circuit"))?;
341 let _ = hash.inputize(cs.namespace(|| "output new hash of this circuit"))?;
342
343 Ok(())
344 }
345}
346
347#[cfg(test)]
348mod tests {
349 use super::*;
350 use crate::bellperson::{shape_cs::ShapeCS, solver::SatisfyingAssignment};
351 type G1 = pasta_curves::pallas::Point;
352 type G2 = pasta_curves::vesta::Point;
353 use crate::constants::{BN_LIMB_WIDTH, BN_N_LIMBS};
354 use crate::{
355 bellperson::r1cs::{NovaShape, NovaWitness},
356 traits::HashFuncConstantsTrait,
357 };
358 use ff::PrimeField;
359 use std::marker::PhantomData;
360
361 struct TestCircuit<F: PrimeField> {
362 _p: PhantomData<F>,
363 }
364
365 impl<F> StepCircuit<F> for TestCircuit<F>
366 where
367 F: PrimeField,
368 {
369 fn synthesize<CS: ConstraintSystem<F>>(
370 &self,
371 _cs: &mut CS,
372 z: AllocatedNum<F>,
373 ) -> Result<AllocatedNum<F>, SynthesisError> {
374 Ok(z)
375 }
376
377 fn compute(&self, z: &F) -> F {
378 *z
379 }
380 }
381
382 #[test]
383 fn test_verification_circuit() {
384 // In the following we use 1 to refer to the primary, and 2 to refer to the secondary circuit
385 let params1 = NIFSVerifierCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS, true);
386 let params2 = NIFSVerifierCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS, false);
387 let ro_consts1: ROConstantsCircuit<<G2 as Group>::Base> = ROConstantsCircuit::new();
388 let ro_consts2: ROConstantsCircuit<<G1 as Group>::Base> = ROConstantsCircuit::new();
389
390 // Initialize the shape and gens for the primary
391 let circuit1: NIFSVerifierCircuit<G2, TestCircuit<<G2 as Group>::Base>> =
392 NIFSVerifierCircuit::new(
393 params1.clone(),
394 None,
395 TestCircuit {
396 _p: Default::default(),
397 },
398 ro_consts1.clone(),
399 );
400 let mut cs: ShapeCS<G1> = ShapeCS::new();
401 let _ = circuit1.synthesize(&mut cs);
402 let (shape1, gens1) = (cs.r1cs_shape(), cs.r1cs_gens());
403 println!(
404 "Circuit1 -> Number of constraints: {}",
405 cs.num_constraints()
406 );
407
408 // Initialize the shape and gens for the secondary
409 let circuit2: NIFSVerifierCircuit<G1, TestCircuit<<G1 as Group>::Base>> =
410 NIFSVerifierCircuit::new(
411 params2.clone(),
412 None,
413 TestCircuit {
414 _p: Default::default(),
415 },
416 ro_consts2.clone(),
417 );
418 let mut cs: ShapeCS<G2> = ShapeCS::new();
419 let _ = circuit2.synthesize(&mut cs);
420 let (shape2, gens2) = (cs.r1cs_shape(), cs.r1cs_gens());
421 println!(
422 "Circuit2 -> Number of constraints: {}",
423 cs.num_constraints()
424 );
425
426 // Execute the base case for the primary
427 let zero1 = <<G2 as Group>::Base as Field>::zero();
428 let mut cs1: SatisfyingAssignment<G1> = SatisfyingAssignment::new();
429 let inputs1: NIFSVerifierCircuitInputs<G2> = NIFSVerifierCircuitInputs::new(
430 shape2.get_digest(),
431 zero1,
432 zero1, // TODO: Provide real input for z0
433 None,
434 None,
435 None,
436 None,
437 );
438 let circuit1: NIFSVerifierCircuit<G2, TestCircuit<<G2 as Group>::Base>> =
439 NIFSVerifierCircuit::new(
440 params1,
441 Some(inputs1),
442 TestCircuit {
443 _p: Default::default(),
444 },
445 ro_consts1,
446 );
447 let _ = circuit1.synthesize(&mut cs1);
448 let (inst1, witness1) = cs1.r1cs_instance_and_witness(&shape1, &gens1).unwrap();
449 // Make sure that this is satisfiable
450 assert!(shape1.is_sat(&gens1, &inst1, &witness1).is_ok());
451
452 // Execute the base case for the secondary
453 let zero2 = <<G1 as Group>::Base as Field>::zero();
454 let mut cs2: SatisfyingAssignment<G2> = SatisfyingAssignment::new();
455 let inputs2: NIFSVerifierCircuitInputs<G1> = NIFSVerifierCircuitInputs::new(
456 shape1.get_digest(),
457 zero2,
458 zero2,
459 None,
460 None,
461 Some(inst1),
462 None,
463 );
464 let circuit: NIFSVerifierCircuit<G1, TestCircuit<<G1 as Group>::Base>> =
465 NIFSVerifierCircuit::new(
466 params2,
467 Some(inputs2),
468 TestCircuit {
469 _p: Default::default(),
470 },
471 ro_consts2,
472 );
473 let _ = circuit.synthesize(&mut cs2);
474 let (inst2, witness2) = cs2.r1cs_instance_and_witness(&shape2, &gens2).unwrap();
475 // Make sure that it is satisfiable
476 assert!(shape2.is_sat(&gens2, &inst2, &witness2).is_ok());
477 }
478}