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