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