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: 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 // 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 /***********************************************************************/
481 // Allocate z0
482 /***********************************************************************/
483
484 let z_0 = AllocatedNum::alloc(cs.namespace(|| "z0"), || Ok(self.inputs.get()?.z0))?;
485
486 /***********************************************************************/
487 // Allocate zi
488 /***********************************************************************/
489
490 let z_i = AllocatedNum::alloc(cs.namespace(|| "zi"), || Ok(self.inputs.get()?.zi))?;
491
492 /***********************************************************************/
493 //Check that if i == 0, z0 = zi, that is (i == 0) AND (z0 != zi) = false
494 /***********************************************************************/
495
496 let z0_is_zi = Boolean::from(alloc_num_equals(
497 cs.namespace(|| "z0 = zi"),
498 z_0.clone(),
499 z_i.clone(),
500 )?);
501
502 cs.enforce(
503 || "i == 0 and z0 != zi = false",
504 |_| base_case.lc(CS::one(), G::Base::one()),
505 |_| z0_is_zi.not().lc(CS::one(), G::Base::one()),
506 |lc| lc,
507 );
508
509 /***********************************************************************/
510 // Check that h1 = Hash(params, u2,i,z0,zi)
511 /***********************************************************************/
512
513 let mut h1_hash: PoseidonROGadget<G::Base> =
514 PoseidonROGadget::new(self.poseidon_constants.clone());
515
516 h1_hash.absorb(params.clone());
517 h1_hash.absorb(W_r.x);
518 h1_hash.absorb(W_r.y);
519 h1_hash.absorb(W_r.is_infinity);
520 h1_hash.absorb(E_r.x);
521 h1_hash.absorb(E_r.y);
522 h1_hash.absorb(E_r.is_infinity);
523 h1_hash.absorb(u_r.clone());
524
525 // absorb each of the limbs of X_r[0]
526 for limb in Xr0_bn.into_iter() {
527 h1_hash.absorb(limb);
528 }
529
530 // absorb each of the limbs of X_r[1]
531 for limb in Xr1_bn.into_iter() {
532 h1_hash.absorb(limb);
533 }
534
535 h1_hash.absorb(i.clone());
536 h1_hash.absorb(z_0.clone());
537 h1_hash.absorb(z_i.clone());
538
539 let hash_bits = h1_hash.get_challenge(cs.namespace(|| "Input hash"))?; // TODO: use get_hash method
540 let hash = le_bits_to_num(cs.namespace(|| "bits to hash"), hash_bits)?;
541
542 cs.enforce(
543 || "check h1",
544 |lc| lc,
545 |lc| lc,
546 |lc| lc + h1.get_variable() - hash.get_variable(),
547 );
548
549 /***********************************************************************/
550 // Compute z_{i+1}
551 /***********************************************************************/
552
553 let z_next = self
554 .step_circuit
555 .synthesize(&mut cs.namespace(|| "F"), z_i)?;
556
557 /***********************************************************************/
558 // Compute the new hash H(params, u2_new, i+1, z0, z_{i+1})
559 /***********************************************************************/
560
561 h1_hash.flush_state();
562 h1_hash.absorb(params);
563 h1_hash.absorb(W_new.x.clone());
564 h1_hash.absorb(W_new.y.clone());
565 h1_hash.absorb(W_new.is_infinity);
566 h1_hash.absorb(E_new.x.clone());
567 h1_hash.absorb(E_new.y.clone());
568 h1_hash.absorb(E_new.is_infinity);
569 h1_hash.absorb(u_new);
570
571 // absorb each of the limbs of X_r_new[0]
572 for limb in Xr0_new_bn.into_iter() {
573 h1_hash.absorb(limb);
574 }
575
576 // absorb each of the limbs of X_r_new[1]
577 for limb in Xr1_new_bn.into_iter() {
578 h1_hash.absorb(limb);
579 }
580
581 h1_hash.absorb(next_i.clone());
582 h1_hash.absorb(z_0);
583 h1_hash.absorb(z_next);
584 let h1_new_bits = h1_hash.get_challenge(cs.namespace(|| "h1_new bits"))?; // TODO: use get_hash method
585 let h1_new = le_bits_to_num(cs.namespace(|| "h1_new"), h1_new_bits)?;
586 let _ = h1_new.inputize(cs.namespace(|| "output h1_new"))?;
587
588 Ok(())
589 }
590}
591
592#[cfg(test)]
593mod tests {
594 use super::*;
595 use crate::bellperson::{shape_cs::ShapeCS, solver::SatisfyingAssignment};
596 type G1 = pasta_curves::pallas::Point;
597 type G2 = pasta_curves::vesta::Point;
598 use crate::{
599 bellperson::r1cs::{NovaShape, NovaWitness},
600 commitments::CommitTrait,
601 };
602 use std::marker::PhantomData;
603
604 struct TestCircuit<F>
605 where
606 F: PrimeField + ff::PrimeField,
607 {
608 _p: PhantomData<F>,
609 }
610
611 impl<F> StepCircuit<F> for TestCircuit<F>
612 where
613 F: PrimeField + ff::PrimeField,
614 {
615 fn synthesize<CS: ConstraintSystem<F>>(
616 &self,
617 _cs: &mut CS,
618 z: AllocatedNum<F>,
619 ) -> Result<AllocatedNum<F>, SynthesisError> {
620 Ok(z)
621 }
622 }
623
624 #[test]
625 fn test_verification_circuit() {
626 // We experiment with 8 limbs of 32 bits each
627 let params = NIFSVerifierCircuitParams::new(32, 8);
628 // The first circuit that verifies G2
629 let poseidon_constants1: NovaPoseidonConstants<<G2 as Group>::Base> =
630 NovaPoseidonConstants::new();
631 let circuit1: NIFSVerifierCircuit<G2, TestCircuit<<G2 as Group>::Base>> =
632 NIFSVerifierCircuit::new(
633 params.clone(),
634 None,
635 TestCircuit {
636 _p: Default::default(),
637 },
638 poseidon_constants1.clone(),
639 );
640 // First create the shape
641 let mut cs: ShapeCS<G1> = ShapeCS::new();
642 let _ = circuit1.synthesize(&mut cs);
643 let (shape1, gens1) = (cs.r1cs_shape(), cs.r1cs_gens());
644 println!(
645 "Circuit1 -> Number of constraints: {}",
646 cs.num_constraints()
647 );
648
649 // The second circuit that verifies G1
650 let poseidon_constants2: NovaPoseidonConstants<<G1 as Group>::Base> =
651 NovaPoseidonConstants::new();
652 let circuit2: NIFSVerifierCircuit<G1, TestCircuit<<G1 as Group>::Base>> =
653 NIFSVerifierCircuit::new(
654 params.clone(),
655 None,
656 TestCircuit {
657 _p: Default::default(),
658 },
659 poseidon_constants2,
660 );
661 // First create the shape
662 let mut cs: ShapeCS<G2> = ShapeCS::new();
663 let _ = circuit2.synthesize(&mut cs);
664 let (shape2, gens2) = (cs.r1cs_shape(), cs.r1cs_gens());
665 println!(
666 "Circuit2 -> Number of constraints: {}",
667 cs.num_constraints()
668 );
669
670 // TODO: We need to hardwire default hash or give it as input
671 let default_hash = <<G2 as Group>::Base as ff::PrimeField>::from_str_vartime(
672 "332553638888022689042501686561503049809",
673 )
674 .unwrap();
675
676 let T = vec![<G2 as Group>::Scalar::zero()].commit(&gens2.gens_E);
677 let w = vec![<G2 as Group>::Scalar::zero()].commit(&gens2.gens_E);
678
679 // Now get an assignment
680 let mut cs: SatisfyingAssignment<G1> = SatisfyingAssignment::new();
681 let inputs: NIFSVerifierCircuitInputs<G2> = NIFSVerifierCircuitInputs::new(
682 default_hash,
683 RelaxedR1CSInstance::default(&gens2, &shape2),
684 <<G2 as Group>::Base as Field>::zero(), // TODO: provide real inputs
685 <<G2 as Group>::Base as Field>::zero(), // TODO: provide real inputs
686 <<G2 as Group>::Base as Field>::zero(), // TODO: provide real inputs
687 <<G2 as Group>::Scalar as Field>::zero(), // TODO: provide real inputs
688 <<G2 as Group>::Base as Field>::zero(), // TODO: provide real inputs
689 T, // TODO: provide real inputs
690 w,
691 );
692
693 let circuit: NIFSVerifierCircuit<G2, TestCircuit<<G2 as Group>::Base>> =
694 NIFSVerifierCircuit::new(
695 params,
696 Some(inputs),
697 TestCircuit {
698 _p: Default::default(),
699 },
700 poseidon_constants1,
701 );
702 let _ = circuit.synthesize(&mut cs);
703 let (inst, witness) = cs.r1cs_instance_and_witness(&shape1, &gens1).unwrap();
704
705 // Make sure that this is satisfiable
706 assert!(shape1.is_sat(&gens1, &inst, &witness).is_ok());
707 }
708}