Nova/src/circuit.rs
src/circuit.rsRaw
1//! There are two Verification Circuits. Each of them is over a Pasta curve but
2//! only one of them executes the next step of the computation by applying the inner function F.
3//! There are also two running relaxed r1cs instances.
4//!
5//! When we build a circuit we denote u1 the running relaxed r1cs instance of
6//! the circuit and u2 the running relaxed r1cs instance of the other circuit.
7//! The circuit takes as input two hashes h1 and h2.
8//! If the circuit applies the inner function F, then
9//! h1 = H(params = H(shape, gens), u2, i, z0, zi) and h2 = H(u1, i)
10//! otherwise
11//! h1 = H(u2, i) and h2 = H(params = H(shape, gens), u1, i, z0, zi)
12
13use super::{
14 commitments::Commitment,
15 gadgets::{
16 ecc::AllocatedPoint,
17 utils::{
18 alloc_bignat_constant, alloc_num_equals, alloc_one, alloc_zero, conditionally_select,
19 conditionally_select_bignat, le_bits_to_num,
20 },
21 },
22 poseidon::{NovaPoseidonConstants, PoseidonROGadget},
23 r1cs::RelaxedR1CSInstance,
24 traits::{Group, StepCircuit},
25};
26use bellperson::{
27 gadgets::{boolean::Boolean, num::AllocatedNum, Assignment},
28 Circuit, ConstraintSystem, SynthesisError,
29};
30use bellperson_nonnative::{
31 mp::bignat::BigNat,
32 util::{convert::f_to_nat, num::Num},
33};
34use ff::{Field, PrimeField, PrimeFieldBits};
35
36#[derive(Debug, Clone)]
37pub struct NIFSVerifierCircuitParams {
38 limb_width: usize,
39 n_limbs: usize,
40}
41
42impl NIFSVerifierCircuitParams {
43 #[allow(dead_code)]
44 pub fn new(limb_width: usize, n_limbs: usize) -> Self {
45 Self {
46 limb_width,
47 n_limbs,
48 }
49 }
50}
51
52pub struct NIFSVerifierCircuitInputs<G>
53where
54 G: Group,
55{
56 h1: G::Base,
57 h2: G::Scalar,
58 u2: RelaxedR1CSInstance<G>,
59 i: G::Base,
60 z0: G::Base,
61 zi: G::Base,
62 params: G::Base, // Hash(Shape of u2, Gens for u2). Needed for computing the challenge.
63 T: Commitment<G>,
64 w: Commitment<G>, // The commitment to the witness of the fresh r1cs instance
65}
66
67impl<G> NIFSVerifierCircuitInputs<G>
68where
69 G: Group,
70{
71 /// Create new inputs/witness for the verification circuit
72 #[allow(dead_code, clippy::too_many_arguments)]
73 pub fn new(
74 h1: G::Base,
75 u2: RelaxedR1CSInstance<G>,
76 i: G::Base,
77 z0: G::Base,
78 zi: G::Base,
79 h2: G::Scalar,
80 params: G::Base,
81 T: Commitment<G>,
82 w: Commitment<G>,
83 ) -> Self {
84 Self {
85 h1,
86 u2,
87 i,
88 z0,
89 zi,
90 h2,
91 params,
92 T,
93 w,
94 }
95 }
96}
97
98/// Circuit that encodes only the folding verifier
99pub struct NIFSVerifierCircuit<G, SC>
100where
101 G: Group,
102 <G as Group>::Base: ff::PrimeField,
103 SC: StepCircuit<G::Base>,
104{
105 params: NIFSVerifierCircuitParams,
106 inputs: Option<NIFSVerifierCircuitInputs<G>>,
107 step_circuit: Option<SC>, // The function that is applied for each step. may be None.
108 poseidon_constants: NovaPoseidonConstants<G::Base>,
109}
110
111impl<G, SC> NIFSVerifierCircuit<G, SC>
112where
113 G: Group,
114 <G as Group>::Base: ff::PrimeField,
115 SC: StepCircuit<G::Base>,
116{
117 /// Create a new verification circuit for the input relaxed r1cs instances
118 #[allow(dead_code)]
119 pub fn new(
120 params: NIFSVerifierCircuitParams,
121 inputs: Option<NIFSVerifierCircuitInputs<G>>,
122 step_circuit: Option<SC>,
123 poseidon_constants: NovaPoseidonConstants<G::Base>,
124 ) -> Self
125 where
126 <G as Group>::Base: ff::PrimeField,
127 {
128 Self {
129 params,
130 inputs,
131 step_circuit,
132 poseidon_constants,
133 }
134 }
135}
136
137impl<G, SC> Circuit<<G as Group>::Base> for NIFSVerifierCircuit<G, SC>
138where
139 G: Group,
140 <G as Group>::Base: PrimeField + PrimeFieldBits,
141 <G as Group>::Scalar: PrimeFieldBits,
142 SC: StepCircuit<G::Base>,
143{
144 fn synthesize<CS: ConstraintSystem<<G as Group>::Base>>(
145 self,
146 cs: &mut CS,
147 ) -> Result<(), SynthesisError> {
148 /***********************************************************************/
149 // This circuit does not modify h2 but it outputs it.
150 // Allocate it and output it.
151 /***********************************************************************/
152
153 // Allocate h2 as a big number with 8 limbs
154 let h2_bn = BigNat::alloc_from_nat(
155 cs.namespace(|| "allocate h2"),
156 || Ok(f_to_nat(&self.inputs.get()?.h2)),
157 self.params.limb_width,
158 self.params.n_limbs,
159 )?;
160
161 let _ = h2_bn.inputize(cs.namespace(|| "Output 1"))?;
162
163 /***********************************************************************/
164 // Allocate h1
165 /***********************************************************************/
166
167 let h1 = AllocatedNum::alloc(cs.namespace(|| "allocate h1"), || Ok(self.inputs.get()?.h1))?;
168 let h1_bn = BigNat::from_num(
169 cs.namespace(|| "allocate h1_bn"),
170 Num::from(h1.clone()),
171 self.params.limb_width,
172 self.params.n_limbs,
173 )?;
174
175 /***********************************************************************/
176 // Allocate u2 by allocating W_r, E_r, u_r, X_r
177 /***********************************************************************/
178
179 // W_r = (x, y, infinity)
180 let W_r = AllocatedPoint::alloc(
181 cs.namespace(|| "allocate W_r"),
182 self
183 .inputs
184 .get()
185 .map_or(None, |inputs| Some(inputs.u2.comm_W.comm.to_coordinates())),
186 )?;
187
188 // E_r = (x, y, infinity)
189 let E_r = AllocatedPoint::alloc(
190 cs.namespace(|| "allocate E_r"),
191 self
192 .inputs
193 .get()
194 .map_or(None, |inputs| Some(inputs.u2.comm_E.comm.to_coordinates())),
195 )?;
196
197 // u_r << |G::Base| despite the fact that u_r is a scalar.
198 // So we parse all of its bytes as a G::Base element
199 let u_r = AllocatedNum::alloc(cs.namespace(|| "u_r"), || {
200 let u_bits = self.inputs.get()?.u2.u.to_le_bits();
201 let mut mult = G::Base::one();
202 let mut u = G::Base::zero();
203 for bit in u_bits {
204 if bit {
205 u += mult;
206 }
207 mult = mult + mult;
208 }
209 Ok(u)
210 })?;
211
212 // The running X is two items! the running h1 and the running h2
213 let Xr0 = BigNat::alloc_from_nat(
214 cs.namespace(|| "allocate X_r[0]"),
215 || Ok(f_to_nat(&self.inputs.get()?.u2.X[0])),
216 self.params.limb_width,
217 self.params.n_limbs,
218 )?;
219
220 // Analyze Xr0 as limbs to use later
221 let Xr0_bn = Xr0
222 .as_limbs::<CS>()
223 .iter()
224 .enumerate()
225 .map(|(i, limb)| {
226 limb
227 .as_sapling_allocated_num(cs.namespace(|| format!("convert limb {} of X_r[0] to num", i)))
228 })
229 .collect::<Result<Vec<AllocatedNum<G::Base>>, _>>()?;
230
231 let Xr1 = BigNat::alloc_from_nat(
232 cs.namespace(|| "allocate X_r[1]"),
233 || Ok(f_to_nat(&self.inputs.get()?.u2.X[1])),
234 self.params.limb_width,
235 self.params.n_limbs,
236 )?;
237
238 // Analyze Xr1 as limbs to use later
239 let Xr1_bn = Xr1
240 .as_limbs::<CS>()
241 .iter()
242 .enumerate()
243 .map(|(i, limb)| {
244 limb
245 .as_sapling_allocated_num(cs.namespace(|| format!("convert limb {} of X_r[1] to num", i)))
246 })
247 .collect::<Result<Vec<AllocatedNum<G::Base>>, _>>()?;
248
249 /***********************************************************************/
250 // Allocate i
251 /***********************************************************************/
252
253 let i = AllocatedNum::alloc(cs.namespace(|| "i"), || Ok(self.inputs.get()?.i))?;
254
255 /***********************************************************************/
256 // Allocate T
257 /***********************************************************************/
258
259 // T = (x, y, infinity)
260
261 let T = AllocatedPoint::alloc(
262 cs.namespace(|| "allocate T"),
263 self
264 .inputs
265 .get()
266 .map_or(None, |inputs| Some(inputs.T.comm.to_coordinates())),
267 )?;
268
269 /***********************************************************************/
270 // Allocate params
271 /***********************************************************************/
272
273 let params = AllocatedNum::alloc(cs.namespace(|| "params"), || Ok(self.inputs.get()?.params))?;
274
275 /***********************************************************************/
276 // Allocate W
277 /***********************************************************************/
278
279 // W = (x, y, infinity)
280 let W = AllocatedPoint::alloc(
281 cs.namespace(|| "allocate W"),
282 self
283 .inputs
284 .get()
285 .map_or(None, |inputs| Some(inputs.w.comm.to_coordinates())),
286 )?;
287
288 /***********************************************************************/
289 // U2' = default if i == 0, otherwise NIFS.V(pp, u_new, U, T)
290 /***********************************************************************/
291
292 //Allocate 0 and 1
293 let zero = alloc_zero(cs.namespace(|| "zero"))?;
294 // Hack: We just do this because the number of inputs must be even!!
295 zero.inputize(cs.namespace(|| "allocate zero as input"))?;
296 let one = alloc_one(cs.namespace(|| "one"))?;
297
298 // Compute default values of U2':
299 let zero_commitment = AllocatedPoint::new(zero.clone(), zero.clone(), one);
300
301 // W_default and E_default are a commitment to zero
302 let W_default = zero_commitment.clone();
303 let E_default = zero_commitment;
304
305 // u_default = 0
306 let u_default = zero.clone();
307
308 // X_default = 0
309 let X0_default = BigNat::alloc_from_nat(
310 cs.namespace(|| "allocate x_default[0]"),
311 || Ok(f_to_nat(&G::Scalar::zero())),
312 self.params.limb_width,
313 self.params.n_limbs,
314 )?;
315
316 let X1_default = BigNat::alloc_from_nat(
317 cs.namespace(|| "allocate x_default[1]"),
318 || Ok(f_to_nat(&G::Scalar::zero())),
319 self.params.limb_width,
320 self.params.n_limbs,
321 )?;
322
323 // Compute r:
324
325 let mut ro: PoseidonROGadget<G::Base> = PoseidonROGadget::new(self.poseidon_constants.clone());
326
327 ro.absorb(h1.clone());
328 // absorb each of the limbs of h2
329 // TODO: Check if it is more efficient to treat h2 as allocNum
330 for (i, limb) in h2_bn.as_limbs::<CS>().iter().enumerate() {
331 let limb_num = limb
332 .as_sapling_allocated_num(cs.namespace(|| format!("convert limb {} of h2 to num", i)))?;
333 ro.absorb(limb_num);
334 }
335 ro.absorb(W.x.clone());
336 ro.absorb(W.y.clone());
337 ro.absorb(W.is_infinity.clone());
338 ro.absorb(T.x.clone());
339 ro.absorb(T.y.clone());
340 ro.absorb(T.is_infinity.clone());
341 // absorb each of the limbs of X_r[0]
342 for limb in Xr0_bn.clone().into_iter() {
343 ro.absorb(limb);
344 }
345
346 // absorb each of the limbs of X_r[1]
347 for limb in Xr1_bn.clone().into_iter() {
348 ro.absorb(limb);
349 }
350
351 let r_bits = ro.get_challenge(cs.namespace(|| "r bits"))?;
352 let r = le_bits_to_num(cs.namespace(|| "r"), r_bits.clone())?;
353
354 // W_fold = W_r + r * W
355 let rW = W.scalar_mul(cs.namespace(|| "r * W"), r_bits.clone())?;
356 let W_fold = W_r.add(cs.namespace(|| "W_r + r * W"), &rW)?;
357
358 // E_fold = E_r + r * T
359 let rT = T.scalar_mul(cs.namespace(|| "r * T"), r_bits)?;
360 let E_fold = E_r.add(cs.namespace(|| "E_r + r * T"), &rT)?;
361
362 // u_fold = u_r + r
363 let u_fold = AllocatedNum::alloc(cs.namespace(|| "u_fold"), || {
364 Ok(*u_r.get_value().get()? + r.get_value().get()?)
365 })?;
366 cs.enforce(
367 || "Check u_fold",
368 |lc| lc,
369 |lc| lc,
370 |lc| lc + u_fold.get_variable() - u_r.get_variable() - r.get_variable(),
371 );
372
373 // Fold the IO:
374 // Analyze r into limbs
375 let r_bn = BigNat::from_num(
376 cs.namespace(|| "allocate r_bn"),
377 Num::from(r.clone()),
378 self.params.limb_width,
379 self.params.n_limbs,
380 )?;
381
382 // Allocate the order of the non-native field as a constant
383 let m_bn = alloc_bignat_constant(
384 cs.namespace(|| "alloc m"),
385 &G::get_order(),
386 self.params.limb_width,
387 self.params.n_limbs,
388 )?;
389
390 // First the fold h1 with X_r[0];
391 let (_, r_0) = h1_bn.mult_mod(cs.namespace(|| "r*h1"), &r_bn, &m_bn)?;
392 // add X_r[0]
393 let r_new_0 = Xr0.add::<CS>(&r_0)?;
394 // Now reduce
395 let Xr0_fold = r_new_0.red_mod(cs.namespace(|| "reduce folded X_r[0]"), &m_bn)?;
396
397 // First the fold h2 with X_r[1];
398 let (_, r_1) = h2_bn.mult_mod(cs.namespace(|| "r*h2"), &r_bn, &m_bn)?;
399 // add X_r[1]
400 let r_new_1 = Xr1.add::<CS>(&r_1)?;
401 // Now reduce
402 let Xr1_fold = r_new_1.red_mod(cs.namespace(|| "reduce folded X_r[1]"), &m_bn)?;
403
404 // Now select the default values if i == 0 otherwise the fold values
405 let base_case = Boolean::from(alloc_num_equals(
406 cs.namespace(|| "Check if base case"),
407 i.clone(),
408 zero,
409 )?);
410
411 let W_new = AllocatedPoint::conditionally_select(
412 cs.namespace(|| "W_new"),
413 &W_default,
414 &W_fold,
415 &base_case,
416 )?;
417
418 let E_new = AllocatedPoint::conditionally_select(
419 cs.namespace(|| "E_new"),
420 &E_default,
421 &E_fold,
422 &base_case,
423 )?;
424
425 let u_new = conditionally_select(cs.namespace(|| "u_new"), &u_default, &u_fold, &base_case)?;
426
427 let Xr0_new = conditionally_select_bignat(
428 cs.namespace(|| "X_r_new[0]"),
429 &X0_default,
430 &Xr0_fold,
431 &base_case,
432 )?;
433
434 // Analyze Xr0_new as limbs to use later
435 let Xr0_new_bn = Xr0_new
436 .as_limbs::<CS>()
437 .iter()
438 .enumerate()
439 .map(|(i, limb)| {
440 limb.as_sapling_allocated_num(
441 cs.namespace(|| format!("convert limb {} of X_r_new[0] to num", i)),
442 )
443 })
444 .collect::<Result<Vec<AllocatedNum<G::Base>>, _>>()?;
445
446 let Xr1_new = conditionally_select_bignat(
447 cs.namespace(|| "X_r_new[1]"),
448 &X1_default,
449 &Xr1_fold,
450 &base_case,
451 )?;
452
453 // Analyze Xr1_new as limbs to use later
454 let Xr1_new_bn = Xr1_new
455 .as_limbs::<CS>()
456 .iter()
457 .enumerate()
458 .map(|(i, limb)| {
459 limb.as_sapling_allocated_num(
460 cs.namespace(|| format!("convert limb {} of X_r_new[1] to num", i)),
461 )
462 })
463 .collect::<Result<Vec<AllocatedNum<G::Base>>, _>>()?;
464
465 /***********************************************************************/
466 // Compute i + 1
467 /***********************************************************************/
468
469 let next_i = AllocatedNum::alloc(cs.namespace(|| "i + 1"), || {
470 Ok(*i.get_value().get()? + G::Base::one())
471 })?;
472
473 cs.enforce(
474 || "check i + 1",
475 |lc| lc,
476 |lc| lc,
477 |lc| lc + next_i.get_variable() - CS::one() - i.get_variable(),
478 );
479
480 if self.step_circuit.is_some() {
481 /***********************************************************************/
482 //Allocate z0
483 /***********************************************************************/
484
485 let z_0 = AllocatedNum::alloc(cs.namespace(|| "z0"), || Ok(self.inputs.get()?.z0))?;
486
487 /***********************************************************************/
488 //Allocate zi
489 /***********************************************************************/
490
491 let z_i = AllocatedNum::alloc(cs.namespace(|| "zi"), || Ok(self.inputs.get()?.zi))?;
492
493 /***********************************************************************/
494 //Check that if i == 0, z0 = zi, that is (i == 0) AND (z0 != zi) = false
495 /***********************************************************************/
496
497 let z0_is_zi = Boolean::from(alloc_num_equals(
498 cs.namespace(|| "z0 = zi"),
499 z_0.clone(),
500 z_i.clone(),
501 )?);
502
503 cs.enforce(
504 || "i == 0 and z0 != zi = false",
505 |_| base_case.lc(CS::one(), G::Base::one()),
506 |_| z0_is_zi.not().lc(CS::one(), G::Base::one()),
507 |lc| lc,
508 );
509
510 /***********************************************************************/
511 // Check that h1 = Hash(params, u2,i,z0,zi)
512 /***********************************************************************/
513
514 let mut h1_hash: PoseidonROGadget<G::Base> =
515 PoseidonROGadget::new(self.poseidon_constants.clone());
516
517 h1_hash.absorb(params.clone());
518 h1_hash.absorb(W_r.x);
519 h1_hash.absorb(W_r.y);
520 h1_hash.absorb(W_r.is_infinity);
521 h1_hash.absorb(E_r.x);
522 h1_hash.absorb(E_r.y);
523 h1_hash.absorb(E_r.is_infinity);
524 h1_hash.absorb(u_r.clone());
525
526 // absorb each of the limbs of X_r[0]
527 for limb in Xr0_bn.into_iter() {
528 h1_hash.absorb(limb);
529 }
530
531 // absorb each of the limbs of X_r[1]
532 for limb in Xr1_bn.into_iter() {
533 h1_hash.absorb(limb);
534 }
535
536 h1_hash.absorb(i.clone());
537 h1_hash.absorb(z_0.clone());
538 h1_hash.absorb(z_i.clone());
539
540 let hash_bits = h1_hash.get_challenge(cs.namespace(|| "Input hash"))?;
541 let hash = le_bits_to_num(cs.namespace(|| "bits to hash"), hash_bits)?;
542
543 cs.enforce(
544 || "check h1",
545 |lc| lc,
546 |lc| lc,
547 |lc| lc + h1.get_variable() - hash.get_variable(),
548 );
549
550 /***********************************************************************/
551 // Compute z_{i+1}
552 /***********************************************************************/
553
554 let z_next = self
555 .step_circuit
556 .unwrap()
557 .synthesize(&mut cs.namespace(|| "F"), z_i)?;
558
559 /***********************************************************************/
560 // Compute the new hash H(params, u2_new, i+1, z0, z_{i+1})
561 /***********************************************************************/
562
563 h1_hash.flush_state();
564 h1_hash.absorb(params);
565 h1_hash.absorb(W_new.x.clone());
566 h1_hash.absorb(W_new.y.clone());
567 h1_hash.absorb(W_new.is_infinity);
568 h1_hash.absorb(E_new.x.clone());
569 h1_hash.absorb(E_new.y.clone());
570 h1_hash.absorb(E_new.is_infinity);
571 h1_hash.absorb(u_new);
572
573 // absorb each of the limbs of X_r_new[0]
574 for limb in Xr0_new_bn.into_iter() {
575 h1_hash.absorb(limb);
576 }
577
578 // absorb each of the limbs of X_r_new[1]
579 for limb in Xr1_new_bn.into_iter() {
580 h1_hash.absorb(limb);
581 }
582
583 h1_hash.absorb(next_i.clone());
584 h1_hash.absorb(z_0);
585 h1_hash.absorb(z_next);
586 let h1_new_bits = h1_hash.get_challenge(cs.namespace(|| "h1_new bits"))?;
587 let h1_new = le_bits_to_num(cs.namespace(|| "h1_new"), h1_new_bits)?;
588 let _ = h1_new.inputize(cs.namespace(|| "output h1_new"))?;
589 } else {
590 /***********************************************************************/
591 // Check that h1 = Hash(params, u2, i)
592 /***********************************************************************/
593
594 let mut h1_hash: PoseidonROGadget<G::Base> = PoseidonROGadget::new(self.poseidon_constants);
595
596 h1_hash.absorb(params.clone());
597 h1_hash.absorb(W_r.x);
598 h1_hash.absorb(W_r.y);
599 h1_hash.absorb(W_r.is_infinity);
600 h1_hash.absorb(E_r.x);
601 h1_hash.absorb(E_r.y);
602 h1_hash.absorb(E_r.is_infinity);
603 h1_hash.absorb(u_r);
604 h1_hash.absorb(i.clone());
605
606 // absorb each of the limbs of X_r[0]
607 for limb in Xr0_bn.into_iter() {
608 h1_hash.absorb(limb);
609 }
610
611 // absorb each of the limbs of X_r[1]
612 for limb in Xr1_bn.into_iter() {
613 h1_hash.absorb(limb);
614 }
615
616 let hash_bits = h1_hash.get_challenge(cs.namespace(|| "Input hash"))?;
617 let hash = le_bits_to_num(cs.namespace(|| "bits to hash"), hash_bits)?;
618
619 cs.enforce(
620 || "check h1",
621 |lc| lc,
622 |lc| lc,
623 |lc| lc + h1.get_variable() - hash.get_variable(),
624 );
625
626 /***********************************************************************/
627 // Compute the new hash H(params, u2')
628 /***********************************************************************/
629
630 h1_hash.flush_state();
631 h1_hash.absorb(params);
632 h1_hash.absorb(W_new.x.clone());
633 h1_hash.absorb(W_new.y.clone());
634 h1_hash.absorb(W_new.is_infinity);
635 h1_hash.absorb(E_new.x.clone());
636 h1_hash.absorb(E_new.y.clone());
637 h1_hash.absorb(E_new.is_infinity);
638 h1_hash.absorb(u_new);
639 h1_hash.absorb(next_i.clone());
640
641 // absorb each of the limbs of X_r_new[0]
642 for limb in Xr0_new_bn.into_iter() {
643 h1_hash.absorb(limb);
644 }
645
646 // absorb each of the limbs of X_r_new[1]
647 for limb in Xr1_new_bn.into_iter() {
648 h1_hash.absorb(limb);
649 }
650
651 let h1_new_bits = h1_hash.get_challenge(cs.namespace(|| "h1_new bits"))?;
652 let h1_new = le_bits_to_num(cs.namespace(|| "h1_new"), h1_new_bits)?;
653 let _ = h1_new.inputize(cs.namespace(|| "output h1_new"))?;
654 }
655
656 Ok(())
657 }
658}
659
660#[cfg(test)]
661mod tests {
662 use super::*;
663 use crate::bellperson::{shape_cs::ShapeCS, solver::SatisfyingAssignment};
664 type G1 = pasta_curves::pallas::Point;
665 type G2 = pasta_curves::vesta::Point;
666 use crate::{
667 bellperson::r1cs::{NovaShape, NovaWitness},
668 commitments::CommitTrait,
669 };
670 use std::marker::PhantomData;
671
672 struct TestCircuit<F>
673 where
674 F: PrimeField + ff::PrimeField,
675 {
676 _p: PhantomData<F>,
677 }
678
679 impl<F> StepCircuit<F> for TestCircuit<F>
680 where
681 F: PrimeField + ff::PrimeField,
682 {
683 fn synthesize<CS: ConstraintSystem<F>>(
684 &self,
685 _cs: &mut CS,
686 z: AllocatedNum<F>,
687 ) -> Result<AllocatedNum<F>, SynthesisError> {
688 Ok(z)
689 }
690 }
691
692 #[test]
693 fn test_verification_circuit() {
694 // We experiment with 8 limbs of 32 bits each
695 let params = NIFSVerifierCircuitParams::new(32, 8);
696 // The first circuit that verifies G2
697 let poseidon_constants1: NovaPoseidonConstants<<G2 as Group>::Base> =
698 NovaPoseidonConstants::new();
699 let circuit1: NIFSVerifierCircuit<G2, TestCircuit<<G2 as Group>::Base>> =
700 NIFSVerifierCircuit::new(
701 params.clone(),
702 None,
703 Some(TestCircuit {
704 _p: Default::default(),
705 }),
706 poseidon_constants1.clone(),
707 );
708 // First create the shape
709 let mut cs: ShapeCS<G1> = ShapeCS::new();
710 let _ = circuit1.synthesize(&mut cs);
711 let (shape1, gens1) = (cs.r1cs_shape(), cs.r1cs_gens());
712 println!(
713 "Circuit1 -> Number of constraints: {}",
714 cs.num_constraints()
715 );
716
717 // The second circuit that verifies G1
718 let poseidon_constants2: NovaPoseidonConstants<<G1 as Group>::Base> =
719 NovaPoseidonConstants::new();
720 let circuit2: NIFSVerifierCircuit<G1, TestCircuit<<G1 as Group>::Base>> =
721 NIFSVerifierCircuit::new(params.clone(), None, None, poseidon_constants2);
722 // First create the shape
723 let mut cs: ShapeCS<G2> = ShapeCS::new();
724 let _ = circuit2.synthesize(&mut cs);
725 let (shape2, gens2) = (cs.r1cs_shape(), cs.r1cs_gens());
726 println!(
727 "Circuit2 -> Number of constraints: {}",
728 cs.num_constraints()
729 );
730
731 // TODO: We need to hardwire default hash or give it as input
732 let default_hash = <<G2 as Group>::Base as ff::PrimeField>::from_str_vartime(
733 "332553638888022689042501686561503049809",
734 )
735 .unwrap();
736
737 let T = vec![<G2 as Group>::Scalar::zero()].commit(&gens2.gens_E);
738 let w = vec![<G2 as Group>::Scalar::zero()].commit(&gens2.gens_E);
739
740 // Now get an assignment
741 let mut cs: SatisfyingAssignment<G1> = SatisfyingAssignment::new();
742 let inputs: NIFSVerifierCircuitInputs<G2> = NIFSVerifierCircuitInputs::new(
743 default_hash,
744 RelaxedR1CSInstance::default(&gens2, &shape2),
745 <<G2 as Group>::Base as Field>::zero(), // TODO: provide real inputs
746 <<G2 as Group>::Base as Field>::zero(), // TODO: provide real inputs
747 <<G2 as Group>::Base as Field>::zero(), // TODO: provide real inputs
748 <<G2 as Group>::Scalar as Field>::zero(), // TODO: provide real inputs
749 <<G2 as Group>::Base as Field>::zero(), // TODO: provide real inputs
750 T, // TODO: provide real inputs
751 w,
752 );
753
754 let circuit: NIFSVerifierCircuit<G2, TestCircuit<<G2 as Group>::Base>> =
755 NIFSVerifierCircuit::new(
756 params,
757 Some(inputs),
758 Some(TestCircuit {
759 _p: Default::default(),
760 }),
761 poseidon_constants1,
762 );
763 let _ = circuit.synthesize(&mut cs);
764 let (inst, witness) = cs.r1cs_instance_and_witness(&shape1, &gens1).unwrap();
765
766 // Make sure that this is satisfiable
767 assert!(shape1.is_sat(&gens1, &inst, &witness).is_ok());
768 }
769}