Nova/src/circuit.rs
src/circuit.rsRaw
1//! There are two Verification Circuits. The primary and the secondary.
2//! Each of them is over a Pasta curve but
3//! only the primary executes the next step of the computation.
4//! We have two running instances. Each circuit takes as input 2 hashes: one for each
5//! of the running instances. Each of these hashes is
6//! H(params = H(shape, gens), i, z0, zi, U). Each circuit folds the last invocation of
7//! the other into the running instance
8
9use super::{
10 commitments::Commitment,
11 constants::{NUM_FE_WITHOUT_IO_FOR_CRHF, NUM_HASH_BITS},
12 gadgets::{
13 ecc::AllocatedPoint,
14 r1cs::{AllocatedR1CSInstance, AllocatedRelaxedR1CSInstance},
15 utils::{
16 alloc_num_equals, alloc_scalar_as_base, alloc_zero, conditionally_select_vec, le_bits_to_num,
17 },
18 },
19 r1cs::{R1CSInstance, RelaxedR1CSInstance},
20 traits::{circuit::StepCircuit, Group, ROCircuitTrait, ROConstantsCircuit},
21};
22use bellperson::{
23 gadgets::{
24 boolean::{AllocatedBit, Boolean},
25 num::AllocatedNum,
26 Assignment,
27 },
28 Circuit, ConstraintSystem, SynthesisError,
29};
30use ff::Field;
31
32#[derive(Debug, Clone)]
33pub struct NovaAugmentedCircuitParams {
34 limb_width: usize,
35 n_limbs: usize,
36 is_primary_circuit: bool, // A boolean indicating if this is the primary circuit
37}
38
39impl NovaAugmentedCircuitParams {
40 pub fn new(limb_width: usize, n_limbs: usize, is_primary_circuit: bool) -> Self {
41 Self {
42 limb_width,
43 n_limbs,
44 is_primary_circuit,
45 }
46 }
47}
48
49#[derive(Debug)]
50pub struct NovaAugmentedCircuitInputs<G: Group> {
51 params: G::Scalar, // Hash(Shape of u2, Gens for u2). Needed for computing the challenge.
52 i: G::Base,
53 z0: Vec<G::Base>,
54 zi: Option<Vec<G::Base>>,
55 U: Option<RelaxedR1CSInstance<G>>,
56 u: Option<R1CSInstance<G>>,
57 T: Option<Commitment<G>>,
58}
59
60impl<G> NovaAugmentedCircuitInputs<G>
61where
62 G: Group,
63{
64 /// Create new inputs/witness for the verification circuit
65 #[allow(clippy::too_many_arguments)]
66 pub fn new(
67 params: G::Scalar,
68 i: G::Base,
69 z0: Vec<G::Base>,
70 zi: Option<Vec<G::Base>>,
71 U: Option<RelaxedR1CSInstance<G>>,
72 u: Option<R1CSInstance<G>>,
73 T: Option<Commitment<G>>,
74 ) -> Self {
75 Self {
76 params,
77 i,
78 z0,
79 zi,
80 U,
81 u,
82 T,
83 }
84 }
85}
86
87/// The augmented circuit F' in Nova that includes a step circuit F
88/// and the circuit for the verifier in Nova's non-interactive folding scheme
89pub struct NovaAugmentedCircuit<G, SC>
90where
91 G: Group,
92 SC: StepCircuit<G::Base>,
93{
94 params: NovaAugmentedCircuitParams,
95 ro_consts: ROConstantsCircuit<G>,
96 inputs: Option<NovaAugmentedCircuitInputs<G>>,
97 step_circuit: SC, // The function that is applied for each step
98}
99
100impl<G, SC> NovaAugmentedCircuit<G, SC>
101where
102 G: Group,
103 SC: StepCircuit<G::Base>,
104{
105 /// Create a new verification circuit for the input relaxed r1cs instances
106 pub fn new(
107 params: NovaAugmentedCircuitParams,
108 inputs: Option<NovaAugmentedCircuitInputs<G>>,
109 step_circuit: SC,
110 ro_consts: ROConstantsCircuit<G>,
111 ) -> Self {
112 Self {
113 params,
114 inputs,
115 step_circuit,
116 ro_consts,
117 }
118 }
119
120 /// Allocate all witnesses and return
121 fn alloc_witness<CS: ConstraintSystem<<G as Group>::Base>>(
122 &self,
123 mut cs: CS,
124 arity: usize,
125 ) -> Result<
126 (
127 AllocatedNum<G::Base>,
128 AllocatedNum<G::Base>,
129 Vec<AllocatedNum<G::Base>>,
130 Vec<AllocatedNum<G::Base>>,
131 AllocatedRelaxedR1CSInstance<G>,
132 AllocatedR1CSInstance<G>,
133 AllocatedPoint<G::Base>,
134 ),
135 SynthesisError,
136 > {
137 // Allocate the params
138 let params = alloc_scalar_as_base::<G, _>(
139 cs.namespace(|| "params"),
140 self.inputs.get().map_or(None, |inputs| Some(inputs.params)),
141 )?;
142
143 // Allocate i
144 let i = AllocatedNum::alloc(cs.namespace(|| "i"), || Ok(self.inputs.get()?.i))?;
145
146 // Allocate z0
147 let z_0 = (0..arity)
148 .map(|i| {
149 AllocatedNum::alloc(cs.namespace(|| format!("z0_{}", i)), || {
150 Ok(self.inputs.get()?.z0[i])
151 })
152 })
153 .collect::<Result<Vec<AllocatedNum<G::Base>>, _>>()?;
154
155 // Allocate zi. If inputs.zi is not provided (base case) allocate default value 0
156 let zero = vec![G::Base::zero(); arity];
157 let z_i = (0..arity)
158 .map(|i| {
159 AllocatedNum::alloc(cs.namespace(|| format!("zi_{}", i)), || {
160 Ok(self.inputs.get()?.zi.as_ref().unwrap_or(&zero)[i])
161 })
162 })
163 .collect::<Result<Vec<AllocatedNum<G::Base>>, _>>()?;
164
165 // Allocate the running instance
166 let U: AllocatedRelaxedR1CSInstance<G> = AllocatedRelaxedR1CSInstance::alloc(
167 cs.namespace(|| "Allocate U"),
168 self.inputs.get().map_or(None, |inputs| {
169 inputs.U.get().map_or(None, |U| Some(U.clone()))
170 }),
171 self.params.limb_width,
172 self.params.n_limbs,
173 )?;
174
175 // Allocate the instance to be folded in
176 let u = AllocatedR1CSInstance::alloc(
177 cs.namespace(|| "allocate instance u to fold"),
178 self.inputs.get().map_or(None, |inputs| {
179 inputs.u.get().map_or(None, |u| Some(u.clone()))
180 }),
181 )?;
182
183 // Allocate T
184 let T = AllocatedPoint::alloc(
185 cs.namespace(|| "allocate T"),
186 self.inputs.get().map_or(None, |inputs| {
187 inputs
188 .T
189 .get()
190 .map_or(None, |T| Some(T.comm.to_coordinates()))
191 }),
192 )?;
193
194 Ok((params, i, z_0, z_i, U, u, T))
195 }
196
197 /// Synthesizes base case and returns the new relaxed R1CSInstance
198 fn synthesize_base_case<CS: ConstraintSystem<<G as Group>::Base>>(
199 &self,
200 mut cs: CS,
201 u: AllocatedR1CSInstance<G>,
202 ) -> Result<AllocatedRelaxedR1CSInstance<G>, SynthesisError> {
203 let U_default: AllocatedRelaxedR1CSInstance<G> = if self.params.is_primary_circuit {
204 // The primary circuit just returns the default R1CS instance
205 AllocatedRelaxedR1CSInstance::default(
206 cs.namespace(|| "Allocate U_default"),
207 self.params.limb_width,
208 self.params.n_limbs,
209 )?
210 } else {
211 // The secondary circuit returns the incoming R1CS instance
212 AllocatedRelaxedR1CSInstance::from_r1cs_instance(
213 cs.namespace(|| "Allocate U_default"),
214 u,
215 self.params.limb_width,
216 self.params.n_limbs,
217 )?
218 };
219 Ok(U_default)
220 }
221
222 /// Synthesizes non base case and returns the new relaxed R1CSInstance
223 /// And a boolean indicating if all checks pass
224 #[allow(clippy::too_many_arguments)]
225 fn synthesize_non_base_case<CS: ConstraintSystem<<G as Group>::Base>>(
226 &self,
227 mut cs: CS,
228 params: AllocatedNum<G::Base>,
229 i: AllocatedNum<G::Base>,
230 z_0: Vec<AllocatedNum<G::Base>>,
231 z_i: Vec<AllocatedNum<G::Base>>,
232 U: AllocatedRelaxedR1CSInstance<G>,
233 u: AllocatedR1CSInstance<G>,
234 T: AllocatedPoint<G::Base>,
235 arity: usize,
236 ) -> Result<(AllocatedRelaxedR1CSInstance<G>, AllocatedBit), SynthesisError> {
237 // Check that u.x[0] = Hash(params, U, i, z0, zi)
238 let mut ro = G::ROCircuit::new(
239 self.ro_consts.clone(),
240 NUM_FE_WITHOUT_IO_FOR_CRHF + 2 * arity,
241 );
242 ro.absorb(params.clone());
243 ro.absorb(i);
244 for e in z_0 {
245 ro.absorb(e);
246 }
247 for e in z_i {
248 ro.absorb(e);
249 }
250 U.absorb_in_ro(cs.namespace(|| "absorb U"), &mut ro)?;
251
252 let hash_bits = ro.squeeze(cs.namespace(|| "Input hash"), NUM_HASH_BITS)?;
253 let hash = le_bits_to_num(cs.namespace(|| "bits to hash"), hash_bits)?;
254 let check_pass = alloc_num_equals(
255 cs.namespace(|| "check consistency of u.X[0] with H(params, U, i, z0, zi)"),
256 &u.X0,
257 &hash,
258 )?;
259
260 // Run NIFS Verifier
261 let U_fold = U.fold_with_r1cs(
262 cs.namespace(|| "compute fold of U and u"),
263 params,
264 u,
265 T,
266 self.ro_consts.clone(),
267 self.params.limb_width,
268 self.params.n_limbs,
269 )?;
270
271 Ok((U_fold, check_pass))
272 }
273}
274
275impl<G, SC> Circuit<<G as Group>::Base> for NovaAugmentedCircuit<G, SC>
276where
277 G: Group,
278 SC: StepCircuit<G::Base>,
279{
280 fn synthesize<CS: ConstraintSystem<<G as Group>::Base>>(
281 self,
282 cs: &mut CS,
283 ) -> Result<(), SynthesisError> {
284 let arity = self.step_circuit.arity();
285
286 // Allocate all witnesses
287 let (params, i, z_0, z_i, U, u, T) =
288 self.alloc_witness(cs.namespace(|| "allocate the circuit witness"), arity)?;
289
290 // Compute variable indicating if this is the base case
291 let zero = alloc_zero(cs.namespace(|| "zero"))?;
292 let is_base_case = alloc_num_equals(cs.namespace(|| "Check if base case"), &i.clone(), &zero)?;
293
294 // Synthesize the circuit for the base case and get the new running instance
295 let Unew_base = self.synthesize_base_case(cs.namespace(|| "base case"), u.clone())?;
296
297 // Synthesize the circuit for the non-base case and get the new running
298 // instance along with a boolean indicating if all checks have passed
299 let (Unew_non_base, check_non_base_pass) = self.synthesize_non_base_case(
300 cs.namespace(|| "synthesize non base case"),
301 params.clone(),
302 i.clone(),
303 z_0.clone(),
304 z_i.clone(),
305 U,
306 u.clone(),
307 T,
308 arity,
309 )?;
310
311 // Either check_non_base_pass=true or we are in the base case
312 let should_be_false = AllocatedBit::nor(
313 cs.namespace(|| "check_non_base_pass nor base_case"),
314 &check_non_base_pass,
315 &is_base_case,
316 )?;
317 cs.enforce(
318 || "check_non_base_pass nor base_case = false",
319 |lc| lc + should_be_false.get_variable(),
320 |lc| lc + CS::one(),
321 |lc| lc,
322 );
323
324 // Compute the U_new
325 let Unew = Unew_base.conditionally_select(
326 cs.namespace(|| "compute U_new"),
327 Unew_non_base,
328 &Boolean::from(is_base_case.clone()),
329 )?;
330
331 // Compute i + 1
332 let i_new = AllocatedNum::alloc(cs.namespace(|| "i + 1"), || {
333 Ok(*i.get_value().get()? + G::Base::one())
334 })?;
335 cs.enforce(
336 || "check i + 1",
337 |lc| lc,
338 |lc| lc,
339 |lc| lc + i_new.get_variable() - CS::one() - i.get_variable(),
340 );
341
342 // Compute z_{i+1}
343 let z_input = conditionally_select_vec(
344 cs.namespace(|| "select input to F"),
345 &z_0,
346 &z_i,
347 &Boolean::from(is_base_case),
348 )?;
349
350 let z_next = self
351 .step_circuit
352 .synthesize(&mut cs.namespace(|| "F"), &z_input)?;
353
354 if z_next.len() != arity {
355 return Err(SynthesisError::IncompatibleLengthVector(
356 "z_next".to_string(),
357 ));
358 }
359
360 // Compute the new hash H(params, Unew, i+1, z0, z_{i+1})
361 let mut ro = G::ROCircuit::new(self.ro_consts, NUM_FE_WITHOUT_IO_FOR_CRHF + 2 * arity);
362 ro.absorb(params);
363 ro.absorb(i_new.clone());
364 for e in z_0 {
365 ro.absorb(e);
366 }
367 for e in z_next {
368 ro.absorb(e);
369 }
370 Unew.absorb_in_ro(cs.namespace(|| "absorb U_new"), &mut ro)?;
371 let hash_bits = ro.squeeze(cs.namespace(|| "output hash bits"), NUM_HASH_BITS)?;
372 let hash = le_bits_to_num(cs.namespace(|| "convert hash to num"), hash_bits)?;
373
374 // Outputs the computed hash and u.X[1] that corresponds to the hash of the other circuit
375 u.X1
376 .inputize(cs.namespace(|| "Output unmodified hash of the other circuit"))?;
377 hash.inputize(cs.namespace(|| "output new hash of this circuit"))?;
378
379 Ok(())
380 }
381}
382
383#[cfg(test)]
384mod tests {
385 use super::*;
386 use crate::bellperson::{shape_cs::ShapeCS, solver::SatisfyingAssignment};
387 type G1 = pasta_curves::pallas::Point;
388 type G2 = pasta_curves::vesta::Point;
389 use crate::constants::{BN_LIMB_WIDTH, BN_N_LIMBS};
390 use crate::{
391 bellperson::r1cs::{NovaShape, NovaWitness},
392 poseidon::PoseidonConstantsCircuit,
393 traits::{circuit::TrivialTestCircuit, ROConstantsTrait},
394 };
395
396 #[test]
397 fn test_recursive_circuit() {
398 // In the following we use 1 to refer to the primary, and 2 to refer to the secondary circuit
399 let params1 = NovaAugmentedCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS, true);
400 let params2 = NovaAugmentedCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS, false);
401 let ro_consts1: ROConstantsCircuit<G2> = PoseidonConstantsCircuit::new();
402 let ro_consts2: ROConstantsCircuit<G1> = PoseidonConstantsCircuit::new();
403
404 // Initialize the shape and gens for the primary
405 let circuit1: NovaAugmentedCircuit<G2, TrivialTestCircuit<<G2 as Group>::Base>> =
406 NovaAugmentedCircuit::new(
407 params1.clone(),
408 None,
409 TrivialTestCircuit::default(),
410 ro_consts1.clone(),
411 );
412 let mut cs: ShapeCS<G1> = ShapeCS::new();
413 let _ = circuit1.synthesize(&mut cs);
414 let (shape1, gens1) = (cs.r1cs_shape(), cs.r1cs_gens());
415 assert_eq!(cs.num_constraints(), 9819);
416
417 // Initialize the shape and gens for the secondary
418 let circuit2: NovaAugmentedCircuit<G1, TrivialTestCircuit<<G1 as Group>::Base>> =
419 NovaAugmentedCircuit::new(
420 params2.clone(),
421 None,
422 TrivialTestCircuit::default(),
423 ro_consts2.clone(),
424 );
425 let mut cs: ShapeCS<G2> = ShapeCS::new();
426 let _ = circuit2.synthesize(&mut cs);
427 let (shape2, gens2) = (cs.r1cs_shape(), cs.r1cs_gens());
428 assert_eq!(cs.num_constraints(), 10351);
429
430 // Execute the base case for the primary
431 let zero1 = <<G2 as Group>::Base as Field>::zero();
432 let mut cs1: SatisfyingAssignment<G1> = SatisfyingAssignment::new();
433 let inputs1: NovaAugmentedCircuitInputs<G2> = NovaAugmentedCircuitInputs::new(
434 shape2.get_digest(),
435 zero1,
436 vec![zero1],
437 None,
438 None,
439 None,
440 None,
441 );
442 let circuit1: NovaAugmentedCircuit<G2, TrivialTestCircuit<<G2 as Group>::Base>> =
443 NovaAugmentedCircuit::new(
444 params1,
445 Some(inputs1),
446 TrivialTestCircuit::default(),
447 ro_consts1,
448 );
449 let _ = circuit1.synthesize(&mut cs1);
450 let (inst1, witness1) = cs1.r1cs_instance_and_witness(&shape1, &gens1).unwrap();
451 // Make sure that this is satisfiable
452 assert!(shape1.is_sat(&gens1, &inst1, &witness1).is_ok());
453
454 // Execute the base case for the secondary
455 let zero2 = <<G1 as Group>::Base as Field>::zero();
456 let mut cs2: SatisfyingAssignment<G2> = SatisfyingAssignment::new();
457 let inputs2: NovaAugmentedCircuitInputs<G1> = NovaAugmentedCircuitInputs::new(
458 shape1.get_digest(),
459 zero2,
460 vec![zero2],
461 None,
462 None,
463 Some(inst1),
464 None,
465 );
466 let circuit: NovaAugmentedCircuit<G1, TrivialTestCircuit<<G1 as Group>::Base>> =
467 NovaAugmentedCircuit::new(
468 params2,
469 Some(inputs2),
470 TrivialTestCircuit::default(),
471 ro_consts2,
472 );
473 let _ = circuit.synthesize(&mut cs2);
474 let (inst2, witness2) = cs2.r1cs_instance_and_witness(&shape2, &gens2).unwrap();
475 // Make sure that it is satisfiable
476 assert!(shape2.is_sat(&gens2, &inst2, &witness2).is_ok());
477 }
478}