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