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