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 let zero_commitment = AllocatedPoint::new(zero.clone(), zero.clone(), one);
299
300 // W_default and E_default are a commitment to zero
301 let W_default = zero_commitment.clone();
302 let E_default = zero_commitment;
303
304 // u_default = 0
305 let u_default = zero.clone();
306
307 // X_default = 0
308 let X0_default = BigNat::alloc_from_nat(
309 cs.namespace(|| "allocate x_default[0]"),
310 || Ok(f_to_nat(&G::Scalar::zero())),
311 self.params.limb_width,
312 self.params.n_limbs,
313 )?;
314
315 let X1_default = BigNat::alloc_from_nat(
316 cs.namespace(|| "allocate x_default[1]"),
317 || Ok(f_to_nat(&G::Scalar::zero())),
318 self.params.limb_width,
319 self.params.n_limbs,
320 )?;
321
322 // Compute r:
323
324 let mut ro: PoseidonROGadget<G::Base> = PoseidonROGadget::new(self.poseidon_constants.clone());
325
326 ro.absorb(h1.clone());
327 ro.absorb(h2);
328 ro.absorb(W.x.clone());
329 ro.absorb(W.y.clone());
330 ro.absorb(W.is_infinity.clone());
331 ro.absorb(T.x.clone());
332 ro.absorb(T.y.clone());
333 ro.absorb(T.is_infinity.clone());
334 // absorb each of the limbs of X_r[0]
335 for limb in Xr0_bn.clone().into_iter() {
336 ro.absorb(limb);
337 }
338
339 // absorb each of the limbs of X_r[1]
340 for limb in Xr1_bn.clone().into_iter() {
341 ro.absorb(limb);
342 }
343
344 let r_bits = ro.get_challenge(cs.namespace(|| "r bits"))?;
345 let r = le_bits_to_num(cs.namespace(|| "r"), r_bits.clone())?;
346
347 // W_fold = W_r + r * W
348 let rW = W.scalar_mul(cs.namespace(|| "r * W"), r_bits.clone())?;
349 let W_fold = W_r.add(cs.namespace(|| "W_r + r * W"), &rW)?;
350
351 // E_fold = E_r + r * T
352 let rT = T.scalar_mul(cs.namespace(|| "r * T"), r_bits)?;
353 let E_fold = E_r.add(cs.namespace(|| "E_r + r * T"), &rT)?;
354
355 // u_fold = u_r + r
356 let u_fold = AllocatedNum::alloc(cs.namespace(|| "u_fold"), || {
357 Ok(*u_r.get_value().get()? + r.get_value().get()?)
358 })?;
359 cs.enforce(
360 || "Check u_fold",
361 |lc| lc,
362 |lc| lc,
363 |lc| lc + u_fold.get_variable() - u_r.get_variable() - r.get_variable(),
364 );
365
366 // Fold the IO:
367 // Analyze r into limbs
368 let r_bn = BigNat::from_num(
369 cs.namespace(|| "allocate r_bn"),
370 Num::from(r.clone()),
371 self.params.limb_width,
372 self.params.n_limbs,
373 )?;
374
375 // Allocate the order of the non-native field as a constant
376 let m_bn = alloc_bignat_constant(
377 cs.namespace(|| "alloc m"),
378 &G::get_order(),
379 self.params.limb_width,
380 self.params.n_limbs,
381 )?;
382
383 // First the fold h1 with X_r[0];
384 let (_, r_0) = h1_bn.mult_mod(cs.namespace(|| "r*h1"), &r_bn, &m_bn)?;
385 // add X_r[0]
386 let r_new_0 = Xr0.add::<CS>(&r_0)?;
387 // Now reduce
388 let Xr0_fold = r_new_0.red_mod(cs.namespace(|| "reduce folded X_r[0]"), &m_bn)?;
389
390 // First the fold h2 with X_r[1];
391 let (_, r_1) = h2_bn.mult_mod(cs.namespace(|| "r*h2"), &r_bn, &m_bn)?;
392 // add X_r[1]
393 let r_new_1 = Xr1.add::<CS>(&r_1)?;
394 // Now reduce
395 let Xr1_fold = r_new_1.red_mod(cs.namespace(|| "reduce folded X_r[1]"), &m_bn)?;
396
397 // Now select the default values if i == 0 otherwise the fold values
398 let base_case = Boolean::from(alloc_num_equals(
399 cs.namespace(|| "Check if base case"),
400 i.clone(),
401 zero,
402 )?);
403
404 let W_new = AllocatedPoint::conditionally_select(
405 cs.namespace(|| "W_new"),
406 &W_default,
407 &W_fold,
408 &base_case,
409 )?;
410
411 let E_new = AllocatedPoint::conditionally_select(
412 cs.namespace(|| "E_new"),
413 &E_default,
414 &E_fold,
415 &base_case,
416 )?;
417
418 let u_new = conditionally_select(cs.namespace(|| "u_new"), &u_default, &u_fold, &base_case)?;
419
420 let Xr0_new = conditionally_select_bignat(
421 cs.namespace(|| "X_r_new[0]"),
422 &X0_default,
423 &Xr0_fold,
424 &base_case,
425 )?;
426
427 // Analyze Xr0_new as limbs to use later
428 let Xr0_new_bn = Xr0_new
429 .as_limbs::<CS>()
430 .iter()
431 .enumerate()
432 .map(|(i, limb)| {
433 limb.as_sapling_allocated_num(
434 cs.namespace(|| format!("convert limb {} of X_r_new[0] to num", i)),
435 )
436 })
437 .collect::<Result<Vec<AllocatedNum<G::Base>>, _>>()?;
438
439 let Xr1_new = conditionally_select_bignat(
440 cs.namespace(|| "X_r_new[1]"),
441 &X1_default,
442 &Xr1_fold,
443 &base_case,
444 )?;
445
446 // Analyze Xr1_new as limbs to use later
447 let Xr1_new_bn = Xr1_new
448 .as_limbs::<CS>()
449 .iter()
450 .enumerate()
451 .map(|(i, limb)| {
452 limb.as_sapling_allocated_num(
453 cs.namespace(|| format!("convert limb {} of X_r_new[1] to num", i)),
454 )
455 })
456 .collect::<Result<Vec<AllocatedNum<G::Base>>, _>>()?;
457
458 /***********************************************************************/
459 // Compute i + 1
460 /***********************************************************************/
461
462 let next_i = AllocatedNum::alloc(cs.namespace(|| "i + 1"), || {
463 Ok(*i.get_value().get()? + G::Base::one())
464 })?;
465
466 cs.enforce(
467 || "check i + 1",
468 |lc| lc,
469 |lc| lc,
470 |lc| lc + next_i.get_variable() - CS::one() - i.get_variable(),
471 );
472
473 /***********************************************************************/
474 // Allocate z0
475 /***********************************************************************/
476
477 let z_0 = AllocatedNum::alloc(cs.namespace(|| "z0"), || Ok(self.inputs.get()?.z0))?;
478
479 /***********************************************************************/
480 // Allocate zi
481 /***********************************************************************/
482
483 let z_i = AllocatedNum::alloc(cs.namespace(|| "zi"), || Ok(self.inputs.get()?.zi))?;
484
485 /***********************************************************************/
486 //Check that if i == 0, z0 = zi, that is (i == 0) AND (z0 != zi) = false
487 /***********************************************************************/
488
489 let z0_is_zi = Boolean::from(alloc_num_equals(
490 cs.namespace(|| "z0 = zi"),
491 z_0.clone(),
492 z_i.clone(),
493 )?);
494
495 cs.enforce(
496 || "i == 0 and z0 != zi = false",
497 |_| base_case.lc(CS::one(), G::Base::one()),
498 |_| z0_is_zi.not().lc(CS::one(), G::Base::one()),
499 |lc| lc,
500 );
501
502 /***********************************************************************/
503 // Check that h1 = Hash(params, u2,i,z0,zi)
504 /***********************************************************************/
505
506 let mut h1_hash: PoseidonROGadget<G::Base> =
507 PoseidonROGadget::new(self.poseidon_constants.clone());
508
509 h1_hash.absorb(params.clone());
510 h1_hash.absorb(W_r.x);
511 h1_hash.absorb(W_r.y);
512 h1_hash.absorb(W_r.is_infinity);
513 h1_hash.absorb(E_r.x);
514 h1_hash.absorb(E_r.y);
515 h1_hash.absorb(E_r.is_infinity);
516 h1_hash.absorb(u_r.clone());
517
518 // absorb each of the limbs of X_r[0]
519 for limb in Xr0_bn.into_iter() {
520 h1_hash.absorb(limb);
521 }
522
523 // absorb each of the limbs of X_r[1]
524 for limb in Xr1_bn.into_iter() {
525 h1_hash.absorb(limb);
526 }
527
528 h1_hash.absorb(i.clone());
529 h1_hash.absorb(z_0.clone());
530 h1_hash.absorb(z_i.clone());
531
532 let hash_bits = h1_hash.get_challenge(cs.namespace(|| "Input hash"))?; // TODO: use get_hash method
533 let hash = le_bits_to_num(cs.namespace(|| "bits to hash"), hash_bits)?;
534
535 cs.enforce(
536 || "check h1",
537 |lc| lc,
538 |lc| lc,
539 |lc| lc + h1.get_variable() - hash.get_variable(),
540 );
541
542 /***********************************************************************/
543 // Compute z_{i+1}
544 /***********************************************************************/
545
546 let z_next = self
547 .step_circuit
548 .synthesize(&mut cs.namespace(|| "F"), z_i)?;
549
550 /***********************************************************************/
551 // Compute the new hash H(params, u2_new, i+1, z0, z_{i+1})
552 /***********************************************************************/
553
554 h1_hash.flush_state();
555 h1_hash.absorb(params);
556 h1_hash.absorb(W_new.x.clone());
557 h1_hash.absorb(W_new.y.clone());
558 h1_hash.absorb(W_new.is_infinity);
559 h1_hash.absorb(E_new.x.clone());
560 h1_hash.absorb(E_new.y.clone());
561 h1_hash.absorb(E_new.is_infinity);
562 h1_hash.absorb(u_new);
563
564 // absorb each of the limbs of X_r_new[0]
565 for limb in Xr0_new_bn.into_iter() {
566 h1_hash.absorb(limb);
567 }
568
569 // absorb each of the limbs of X_r_new[1]
570 for limb in Xr1_new_bn.into_iter() {
571 h1_hash.absorb(limb);
572 }
573
574 h1_hash.absorb(next_i.clone());
575 h1_hash.absorb(z_0);
576 h1_hash.absorb(z_next);
577 let h1_new_bits = h1_hash.get_challenge(cs.namespace(|| "h1_new bits"))?; // TODO: use get_hash method
578 let h1_new = le_bits_to_num(cs.namespace(|| "h1_new"), h1_new_bits)?;
579 let _ = h1_new.inputize(cs.namespace(|| "output h1_new"))?;
580
581 Ok(())
582 }
583}
584
585#[cfg(test)]
586mod tests {
587 use super::*;
588 use crate::bellperson::{shape_cs::ShapeCS, solver::SatisfyingAssignment};
589 type G1 = pasta_curves::pallas::Point;
590 type G2 = pasta_curves::vesta::Point;
591 use crate::{
592 bellperson::r1cs::{NovaShape, NovaWitness},
593 commitments::CommitTrait,
594 };
595 use std::marker::PhantomData;
596
597 struct TestCircuit<F>
598 where
599 F: PrimeField + ff::PrimeField,
600 {
601 _p: PhantomData<F>,
602 }
603
604 impl<F> StepCircuit<F> for TestCircuit<F>
605 where
606 F: PrimeField + ff::PrimeField,
607 {
608 fn synthesize<CS: ConstraintSystem<F>>(
609 &self,
610 _cs: &mut CS,
611 z: AllocatedNum<F>,
612 ) -> Result<AllocatedNum<F>, SynthesisError> {
613 Ok(z)
614 }
615 }
616
617 #[test]
618 fn test_verification_circuit() {
619 // We experiment with 8 limbs of 32 bits each
620 let params = NIFSVerifierCircuitParams::new(32, 8);
621 // The first circuit that verifies G2
622 let poseidon_constants1: NovaPoseidonConstants<<G2 as Group>::Base> =
623 NovaPoseidonConstants::new();
624 let circuit1: NIFSVerifierCircuit<G2, TestCircuit<<G2 as Group>::Base>> =
625 NIFSVerifierCircuit::new(
626 params.clone(),
627 None,
628 TestCircuit {
629 _p: Default::default(),
630 },
631 poseidon_constants1.clone(),
632 );
633 // First create the shape
634 let mut cs: ShapeCS<G1> = ShapeCS::new();
635 let _ = circuit1.synthesize(&mut cs);
636 let (shape1, gens1) = (cs.r1cs_shape(), cs.r1cs_gens());
637 println!(
638 "Circuit1 -> Number of constraints: {}",
639 cs.num_constraints()
640 );
641
642 // The second circuit that verifies G1
643 let poseidon_constants2: NovaPoseidonConstants<<G1 as Group>::Base> =
644 NovaPoseidonConstants::new();
645 let circuit2: NIFSVerifierCircuit<G1, TestCircuit<<G1 as Group>::Base>> =
646 NIFSVerifierCircuit::new(
647 params.clone(),
648 None,
649 TestCircuit {
650 _p: Default::default(),
651 },
652 poseidon_constants2,
653 );
654 // First create the shape
655 let mut cs: ShapeCS<G2> = ShapeCS::new();
656 let _ = circuit2.synthesize(&mut cs);
657 let (shape2, gens2) = (cs.r1cs_shape(), cs.r1cs_gens());
658 println!(
659 "Circuit2 -> Number of constraints: {}",
660 cs.num_constraints()
661 );
662
663 // TODO: We need to hardwire default hash or give it as input
664 let default_hash = <<G2 as Group>::Base as ff::PrimeField>::from_str_vartime(
665 "332553638888022689042501686561503049809",
666 )
667 .unwrap();
668
669 let T = vec![<G2 as Group>::Scalar::zero()].commit(&gens2.gens_E);
670 let w = vec![<G2 as Group>::Scalar::zero()].commit(&gens2.gens_E);
671
672 // Now get an assignment
673 let mut cs: SatisfyingAssignment<G1> = SatisfyingAssignment::new();
674 let inputs: NIFSVerifierCircuitInputs<G2> = NIFSVerifierCircuitInputs::new(
675 default_hash,
676 RelaxedR1CSInstance::default(&gens2, &shape2),
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 <<G2 as Group>::Base as Field>::zero(), // TODO: provide real inputs
681 <<G2 as Group>::Base as Field>::zero(), // TODO: provide real inputs
682 T, // TODO: provide real inputs
683 w,
684 );
685
686 let circuit: NIFSVerifierCircuit<G2, TestCircuit<<G2 as Group>::Base>> =
687 NIFSVerifierCircuit::new(
688 params,
689 Some(inputs),
690 TestCircuit {
691 _p: Default::default(),
692 },
693 poseidon_constants1,
694 );
695 let _ = circuit.synthesize(&mut cs);
696 let (inst, witness) = cs.r1cs_instance_and_witness(&shape1, &gens1).unwrap();
697
698 // Make sure that this is satisfiable
699 assert!(shape1.is_sat(&gens1, &inst, &witness).is_ok());
700 }
701}