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