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::Base,
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::Base,
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: SC, // The function that is applied for each step
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: 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 // Allocate h1
150 /***********************************************************************/
151
152 let h1 = AllocatedNum::alloc(cs.namespace(|| "allocate h1"), || Ok(self.inputs.get()?.h1))?;
153 let h1_bn = BigNat::from_num(
154 cs.namespace(|| "allocate h1_bn"),
155 Num::from(h1.clone()),
156 self.params.limb_width,
157 self.params.n_limbs,
158 )?;
159
160 /***********************************************************************/
161 // This circuit does not modify h2 but it outputs it.
162 // Allocate it and output it.
163 /***********************************************************************/
164
165 // Allocate h2 as a big number with 8 limbs
166 let h2 = AllocatedNum::alloc(cs.namespace(|| "allocate h2"), || Ok(self.inputs.get()?.h2))?;
167 let h2_bn = BigNat::from_num(
168 cs.namespace(|| "allocate h2_bn"),
169 Num::from(h2.clone()),
170 self.params.limb_width,
171 self.params.n_limbs,
172 )?;
173
174 let _ = h2.inputize(cs.namespace(|| "Output 1"))?;
175
176 /***********************************************************************/
177 // Allocate u2 by allocating W_r, E_r, u_r, X_r
178 /***********************************************************************/
179
180 // W_r = (x, y, infinity)
181 let W_r = AllocatedPoint::alloc(
182 cs.namespace(|| "allocate W_r"),
183 self
184 .inputs
185 .get()
186 .map_or(None, |inputs| Some(inputs.u2.comm_W.comm.to_coordinates())),
187 )?;
188
189 // E_r = (x, y, infinity)
190 let E_r = AllocatedPoint::alloc(
191 cs.namespace(|| "allocate E_r"),
192 self
193 .inputs
194 .get()
195 .map_or(None, |inputs| Some(inputs.u2.comm_E.comm.to_coordinates())),
196 )?;
197
198 // u_r << |G::Base| despite the fact that u_r is a scalar.
199 // So we parse all of its bytes as a G::Base element
200 let u_r = AllocatedNum::alloc(cs.namespace(|| "u_r"), || {
201 let u_bits = self.inputs.get()?.u2.u.to_le_bits();
202 let mut mult = G::Base::one();
203 let mut u = G::Base::zero();
204 for bit in u_bits {
205 if bit {
206 u += mult;
207 }
208 mult = mult + mult;
209 }
210 Ok(u)
211 })?;
212
213 // The running X is two items! the running h1 and the running h2
214 let Xr0 = BigNat::alloc_from_nat(
215 cs.namespace(|| "allocate X_r[0]"),
216 || Ok(f_to_nat(&self.inputs.get()?.u2.X[0])),
217 self.params.limb_width,
218 self.params.n_limbs,
219 )?;
220
221 // Analyze Xr0 as limbs to use later
222 let Xr0_bn = Xr0
223 .as_limbs::<CS>()
224 .iter()
225 .enumerate()
226 .map(|(i, limb)| {
227 limb
228 .as_sapling_allocated_num(cs.namespace(|| format!("convert limb {} of X_r[0] to num", i)))
229 })
230 .collect::<Result<Vec<AllocatedNum<G::Base>>, _>>()?;
231
232 let Xr1 = BigNat::alloc_from_nat(
233 cs.namespace(|| "allocate X_r[1]"),
234 || Ok(f_to_nat(&self.inputs.get()?.u2.X[1])),
235 self.params.limb_width,
236 self.params.n_limbs,
237 )?;
238
239 // Analyze Xr1 as limbs to use later
240 let Xr1_bn = Xr1
241 .as_limbs::<CS>()
242 .iter()
243 .enumerate()
244 .map(|(i, limb)| {
245 limb
246 .as_sapling_allocated_num(cs.namespace(|| format!("convert limb {} of X_r[1] to num", i)))
247 })
248 .collect::<Result<Vec<AllocatedNum<G::Base>>, _>>()?;
249
250 /***********************************************************************/
251 // Allocate i
252 /***********************************************************************/
253
254 let i = AllocatedNum::alloc(cs.namespace(|| "i"), || Ok(self.inputs.get()?.i))?;
255
256 /***********************************************************************/
257 // Allocate T
258 /***********************************************************************/
259
260 // T = (x, y, infinity)
261
262 let T = AllocatedPoint::alloc(
263 cs.namespace(|| "allocate T"),
264 self
265 .inputs
266 .get()
267 .map_or(None, |inputs| Some(inputs.T.comm.to_coordinates())),
268 )?;
269
270 /***********************************************************************/
271 // Allocate params
272 /***********************************************************************/
273
274 let params = AllocatedNum::alloc(cs.namespace(|| "params"), || Ok(self.inputs.get()?.params))?;
275
276 /***********************************************************************/
277 // Allocate W
278 /***********************************************************************/
279
280 // W = (x, y, infinity)
281 let W = AllocatedPoint::alloc(
282 cs.namespace(|| "allocate W"),
283 self
284 .inputs
285 .get()
286 .map_or(None, |inputs| Some(inputs.w.comm.to_coordinates())),
287 )?;
288
289 /***********************************************************************/
290 // U2' = default if i == 0, otherwise NIFS.V(pp, u_new, U, T)
291 /***********************************************************************/
292
293 // Allocate 0 and 1
294 let zero = alloc_zero(cs.namespace(|| "zero"))?;
295 let one = alloc_one(cs.namespace(|| "one"))?;
296
297 // Compute default values of U2':
298 // W_default and E_default are a commitment to zero
299 let W_default = AllocatedPoint::new(zero.clone(), zero.clone(), one);
300 let E_default = W_default.clone();
301
302 // u_default = 0
303 let u_default = zero.clone();
304
305 // X_default = 0
306 let X0_default = BigNat::alloc_from_nat(
307 cs.namespace(|| "allocate x_default[0]"),
308 || Ok(f_to_nat(&G::Scalar::zero())),
309 self.params.limb_width,
310 self.params.n_limbs,
311 )?;
312
313 let X1_default = BigNat::alloc_from_nat(
314 cs.namespace(|| "allocate x_default[1]"),
315 || Ok(f_to_nat(&G::Scalar::zero())),
316 self.params.limb_width,
317 self.params.n_limbs,
318 )?;
319
320 // Compute r:
321
322 let mut ro: PoseidonROGadget<G::Base> = PoseidonROGadget::new(self.poseidon_constants.clone());
323
324 ro.absorb(h1.clone());
325 ro.absorb(h2);
326 ro.absorb(W.x.clone());
327 ro.absorb(W.y.clone());
328 ro.absorb(W.is_infinity.clone());
329 ro.absorb(T.x.clone());
330 ro.absorb(T.y.clone());
331 ro.absorb(T.is_infinity.clone());
332 // absorb each of the limbs of X_r[0]
333 for limb in Xr0_bn.clone().into_iter() {
334 ro.absorb(limb);
335 }
336
337 // absorb each of the limbs of X_r[1]
338 for limb in Xr1_bn.clone().into_iter() {
339 ro.absorb(limb);
340 }
341
342 let r_bits = ro.get_challenge(cs.namespace(|| "r bits"))?;
343 let r = le_bits_to_num(cs.namespace(|| "r"), r_bits.clone())?;
344
345 // W_fold = W_r + r * W
346 let rW = W.scalar_mul(cs.namespace(|| "r * W"), r_bits.clone())?;
347 let W_fold = W_r.add(cs.namespace(|| "W_r + r * W"), &rW)?;
348
349 // E_fold = E_r + r * T
350 let rT = T.scalar_mul(cs.namespace(|| "r * T"), r_bits)?;
351 let E_fold = E_r.add(cs.namespace(|| "E_r + r * T"), &rT)?;
352
353 // u_fold = u_r + r
354 let u_fold = AllocatedNum::alloc(cs.namespace(|| "u_fold"), || {
355 Ok(*u_r.get_value().get()? + r.get_value().get()?)
356 })?;
357 cs.enforce(
358 || "Check u_fold",
359 |lc| lc,
360 |lc| lc,
361 |lc| lc + u_fold.get_variable() - u_r.get_variable() - r.get_variable(),
362 );
363
364 // Fold the IO:
365 // Analyze r into limbs
366 let r_bn = BigNat::from_num(
367 cs.namespace(|| "allocate r_bn"),
368 Num::from(r.clone()),
369 self.params.limb_width,
370 self.params.n_limbs,
371 )?;
372
373 // Allocate the order of the non-native field as a constant
374 let m_bn = alloc_bignat_constant(
375 cs.namespace(|| "alloc m"),
376 &G::get_order(),
377 self.params.limb_width,
378 self.params.n_limbs,
379 )?;
380
381 // First the fold h1 with X_r[0];
382 let (_, r_0) = h1_bn.mult_mod(cs.namespace(|| "r*h1"), &r_bn, &m_bn)?;
383 // add X_r[0]
384 let r_new_0 = Xr0.add::<CS>(&r_0)?;
385 // Now reduce
386 let Xr0_fold = r_new_0.red_mod(cs.namespace(|| "reduce folded X_r[0]"), &m_bn)?;
387
388 // First the fold h2 with X_r[1];
389 let (_, r_1) = h2_bn.mult_mod(cs.namespace(|| "r*h2"), &r_bn, &m_bn)?;
390 // add X_r[1]
391 let r_new_1 = Xr1.add::<CS>(&r_1)?;
392 // Now reduce
393 let Xr1_fold = r_new_1.red_mod(cs.namespace(|| "reduce folded X_r[1]"), &m_bn)?;
394
395 // Now select the default values if i == 0 otherwise the fold values
396 let is_base_case = Boolean::from(alloc_num_equals(
397 cs.namespace(|| "Check if base case"),
398 i.clone(),
399 zero,
400 )?);
401
402 let W_new = AllocatedPoint::conditionally_select(
403 cs.namespace(|| "W_new"),
404 &W_default,
405 &W_fold,
406 &is_base_case,
407 )?;
408
409 let E_new = AllocatedPoint::conditionally_select(
410 cs.namespace(|| "E_new"),
411 &E_default,
412 &E_fold,
413 &is_base_case,
414 )?;
415
416 let u_new = conditionally_select(cs.namespace(|| "u_new"), &u_default, &u_fold, &is_base_case)?;
417
418 let Xr0_new = conditionally_select_bignat(
419 cs.namespace(|| "X_r_new[0]"),
420 &X0_default,
421 &Xr0_fold,
422 &is_base_case,
423 )?;
424
425 // Analyze Xr0_new as limbs to use later
426 let Xr0_new_bn = Xr0_new
427 .as_limbs::<CS>()
428 .iter()
429 .enumerate()
430 .map(|(i, limb)| {
431 limb.as_sapling_allocated_num(
432 cs.namespace(|| format!("convert limb {} of X_r_new[0] to num", i)),
433 )
434 })
435 .collect::<Result<Vec<AllocatedNum<G::Base>>, _>>()?;
436
437 let Xr1_new = conditionally_select_bignat(
438 cs.namespace(|| "X_r_new[1]"),
439 &X1_default,
440 &Xr1_fold,
441 &is_base_case,
442 )?;
443
444 // Analyze Xr1_new as limbs to use later
445 let Xr1_new_bn = Xr1_new
446 .as_limbs::<CS>()
447 .iter()
448 .enumerate()
449 .map(|(i, limb)| {
450 limb.as_sapling_allocated_num(
451 cs.namespace(|| format!("convert limb {} of X_r_new[1] to num", i)),
452 )
453 })
454 .collect::<Result<Vec<AllocatedNum<G::Base>>, _>>()?;
455
456 /***********************************************************************/
457 // Compute i + 1
458 /***********************************************************************/
459
460 let i_new = AllocatedNum::alloc(cs.namespace(|| "i + 1"), || {
461 Ok(*i.get_value().get()? + G::Base::one())
462 })?;
463
464 cs.enforce(
465 || "check i + 1",
466 |lc| lc,
467 |lc| lc,
468 |lc| lc + i_new.get_variable() - CS::one() - i.get_variable(),
469 );
470
471 /***********************************************************************/
472 // Allocate z0
473 /***********************************************************************/
474
475 let z_0 = AllocatedNum::alloc(cs.namespace(|| "z0"), || Ok(self.inputs.get()?.z0))?;
476
477 /***********************************************************************/
478 // Allocate zi
479 /***********************************************************************/
480
481 let z_i = AllocatedNum::alloc(cs.namespace(|| "zi"), || Ok(self.inputs.get()?.zi))?;
482
483 /***********************************************************************/
484 //Check that if i == 0, z0 = zi, that is (i == 0) AND (z0 != zi) = false
485 /***********************************************************************/
486
487 let z0_is_zi = Boolean::from(alloc_num_equals(
488 cs.namespace(|| "z0 = zi"),
489 z_0.clone(),
490 z_i.clone(),
491 )?);
492
493 cs.enforce(
494 || "i == 0 and z0 != zi = false",
495 |_| is_base_case.lc(CS::one(), G::Base::one()),
496 |_| z0_is_zi.not().lc(CS::one(), G::Base::one()),
497 |lc| lc,
498 );
499
500 /***********************************************************************/
501 // Check that h1 = Hash(params, u2,i,z0,zi)
502 /***********************************************************************/
503
504 let mut h1_hash: PoseidonROGadget<G::Base> =
505 PoseidonROGadget::new(self.poseidon_constants.clone());
506
507 h1_hash.absorb(params.clone());
508 h1_hash.absorb(W_r.x);
509 h1_hash.absorb(W_r.y);
510 h1_hash.absorb(W_r.is_infinity);
511 h1_hash.absorb(E_r.x);
512 h1_hash.absorb(E_r.y);
513 h1_hash.absorb(E_r.is_infinity);
514 h1_hash.absorb(u_r.clone());
515
516 // absorb each of the limbs of X_r[0]
517 for limb in Xr0_bn.into_iter() {
518 h1_hash.absorb(limb);
519 }
520
521 // absorb each of the limbs of X_r[1]
522 for limb in Xr1_bn.into_iter() {
523 h1_hash.absorb(limb);
524 }
525
526 h1_hash.absorb(i.clone());
527 h1_hash.absorb(z_0.clone());
528 h1_hash.absorb(z_i.clone());
529
530 let hash_bits = h1_hash.get_challenge(cs.namespace(|| "Input hash"))?; // TODO: use get_hash method
531 let hash = le_bits_to_num(cs.namespace(|| "bits to hash"), hash_bits)?;
532
533 cs.enforce(
534 || "check h1",
535 |lc| lc,
536 |lc| lc,
537 |lc| lc + h1.get_variable() - hash.get_variable(),
538 );
539
540 /***********************************************************************/
541 // Compute z_{i+1}
542 /***********************************************************************/
543
544 let z_next = self
545 .step_circuit
546 .synthesize(&mut cs.namespace(|| "F"), z_i)?;
547
548 /***********************************************************************/
549 // Compute the new hash H(params, u2_new, i+1, z0, z_{i+1})
550 /***********************************************************************/
551
552 h1_hash.flush_state();
553 h1_hash.absorb(params);
554 h1_hash.absorb(W_new.x.clone());
555 h1_hash.absorb(W_new.y.clone());
556 h1_hash.absorb(W_new.is_infinity);
557 h1_hash.absorb(E_new.x.clone());
558 h1_hash.absorb(E_new.y.clone());
559 h1_hash.absorb(E_new.is_infinity);
560 h1_hash.absorb(u_new);
561
562 // absorb each of the limbs of X_r_new[0]
563 for limb in Xr0_new_bn.into_iter() {
564 h1_hash.absorb(limb);
565 }
566
567 // absorb each of the limbs of X_r_new[1]
568 for limb in Xr1_new_bn.into_iter() {
569 h1_hash.absorb(limb);
570 }
571
572 h1_hash.absorb(i_new.clone());
573 h1_hash.absorb(z_0);
574 h1_hash.absorb(z_next);
575 let h1_new_bits = h1_hash.get_challenge(cs.namespace(|| "h1_new bits"))?; // TODO: use get_hash method
576 let h1_new = le_bits_to_num(cs.namespace(|| "h1_new"), h1_new_bits)?;
577 let _ = h1_new.inputize(cs.namespace(|| "output h1_new"))?;
578
579 Ok(())
580 }
581}
582
583#[cfg(test)]
584mod tests {
585 use super::*;
586 use crate::bellperson::{shape_cs::ShapeCS, solver::SatisfyingAssignment};
587 type G1 = pasta_curves::pallas::Point;
588 type G2 = pasta_curves::vesta::Point;
589 use crate::{
590 bellperson::r1cs::{NovaShape, NovaWitness},
591 commitments::CommitTrait,
592 };
593 use std::marker::PhantomData;
594
595 struct TestCircuit<F>
596 where
597 F: PrimeField + ff::PrimeField,
598 {
599 _p: PhantomData<F>,
600 }
601
602 impl<F> StepCircuit<F> for TestCircuit<F>
603 where
604 F: PrimeField + ff::PrimeField,
605 {
606 fn synthesize<CS: ConstraintSystem<F>>(
607 &self,
608 _cs: &mut CS,
609 z: AllocatedNum<F>,
610 ) -> Result<AllocatedNum<F>, SynthesisError> {
611 Ok(z)
612 }
613 }
614
615 #[test]
616 fn test_verification_circuit() {
617 // We experiment with 8 limbs of 32 bits each
618 let params = NIFSVerifierCircuitParams::new(32, 8);
619 // The first circuit that verifies G2
620 let poseidon_constants1: NovaPoseidonConstants<<G2 as Group>::Base> =
621 NovaPoseidonConstants::new();
622 let circuit1: NIFSVerifierCircuit<G2, TestCircuit<<G2 as Group>::Base>> =
623 NIFSVerifierCircuit::new(
624 params.clone(),
625 None,
626 TestCircuit {
627 _p: Default::default(),
628 },
629 poseidon_constants1.clone(),
630 );
631 // First create the shape
632 let mut cs: ShapeCS<G1> = ShapeCS::new();
633 let _ = circuit1.synthesize(&mut cs);
634 let (shape1, gens1) = (cs.r1cs_shape(), cs.r1cs_gens());
635 println!(
636 "Circuit1 -> Number of constraints: {}",
637 cs.num_constraints()
638 );
639
640 // The second circuit that verifies G1
641 let poseidon_constants2: NovaPoseidonConstants<<G1 as Group>::Base> =
642 NovaPoseidonConstants::new();
643 let circuit2: NIFSVerifierCircuit<G1, TestCircuit<<G1 as Group>::Base>> =
644 NIFSVerifierCircuit::new(
645 params.clone(),
646 None,
647 TestCircuit {
648 _p: Default::default(),
649 },
650 poseidon_constants2,
651 );
652 // First create the shape
653 let mut cs: ShapeCS<G2> = ShapeCS::new();
654 let _ = circuit2.synthesize(&mut cs);
655 let (shape2, gens2) = (cs.r1cs_shape(), cs.r1cs_gens());
656 println!(
657 "Circuit2 -> Number of constraints: {}",
658 cs.num_constraints()
659 );
660
661 // TODO: We need to hardwire default hash or give it as input
662 let default_hash = <<G2 as Group>::Base as ff::PrimeField>::from_str_vartime(
663 "332553638888022689042501686561503049809",
664 )
665 .unwrap();
666
667 let T = vec![<G2 as Group>::Scalar::zero()].commit(&gens2.gens_E);
668 let w = vec![<G2 as Group>::Scalar::zero()].commit(&gens2.gens_E);
669
670 // Now get an assignment
671 let mut cs: SatisfyingAssignment<G1> = SatisfyingAssignment::new();
672 let inputs: NIFSVerifierCircuitInputs<G2> = NIFSVerifierCircuitInputs::new(
673 default_hash,
674 RelaxedR1CSInstance::default(&gens2, &shape2),
675 <<G2 as Group>::Base as Field>::zero(), // TODO: provide real inputs
676 <<G2 as Group>::Base as Field>::zero(), // TODO: provide real inputs
677 <<G2 as Group>::Base as Field>::zero(), // TODO: provide real inputs
678 <<G2 as Group>::Base as Field>::zero(), // TODO: provide real inputs
679 <<G2 as Group>::Base as Field>::zero(), // TODO: provide real inputs
680 T, // TODO: provide real inputs
681 w,
682 );
683
684 let circuit: NIFSVerifierCircuit<G2, TestCircuit<<G2 as Group>::Base>> =
685 NIFSVerifierCircuit::new(
686 params,
687 Some(inputs),
688 TestCircuit {
689 _p: Default::default(),
690 },
691 poseidon_constants1,
692 );
693 let _ = circuit.synthesize(&mut cs);
694 let (inst, witness) = cs.r1cs_instance_and_witness(&shape1, &gens1).unwrap();
695
696 // Make sure that this is satisfiable
697 assert!(shape1.is_sat(&gens1, &inst, &witness).is_ok());
698 }
699}