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 gadgets::{
12 ecc::AllocatedPoint,
13 r1cs::{AllocatedR1CSInstance, AllocatedRelaxedR1CSInstance},
14 utils::{
15 alloc_num_equals, alloc_scalar_as_base, alloc_zero, conditionally_select, le_bits_to_num,
16 },
17 },
18 poseidon::{PoseidonROGadget, ROConstantsCircuit},
19 r1cs::{R1CSInstance, RelaxedR1CSInstance},
20 traits::{Group, StepCircuit},
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 NIFSVerifierCircuitParams {
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 NIFSVerifierCircuitParams {
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 NIFSVerifierCircuitInputs<G: Group> {
51 params: G::Scalar, // Hash(Shape of u2, Gens for u2). Needed for computing the challenge.
52 i: G::Base,
53 z0: G::Base,
54 zi: Option<G::Base>,
55 U: Option<RelaxedR1CSInstance<G>>,
56 u: Option<R1CSInstance<G>>,
57 T: Option<Commitment<G>>,
58}
59
60impl<G> NIFSVerifierCircuitInputs<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: G::Base,
70 zi: Option<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/// Circuit that encodes only the folding verifier
88pub struct NIFSVerifierCircuit<G, SC>
89where
90 G: Group,
91 SC: StepCircuit<G::Base>,
92{
93 params: NIFSVerifierCircuitParams,
94 ro_consts: ROConstantsCircuit<G::Base>,
95 inputs: Option<NIFSVerifierCircuitInputs<G>>,
96 step_circuit: SC, // The function that is applied for each step
97}
98
99impl<G, SC> NIFSVerifierCircuit<G, SC>
100where
101 G: Group,
102 SC: StepCircuit<G::Base>,
103{
104 /// Create a new verification circuit for the input relaxed r1cs instances
105 pub fn new(
106 params: NIFSVerifierCircuitParams,
107 inputs: Option<NIFSVerifierCircuitInputs<G>>,
108 step_circuit: SC,
109 ro_consts: ROConstantsCircuit<G::Base>,
110 ) -> Self {
111 Self {
112 params,
113 inputs,
114 step_circuit,
115 ro_consts,
116 }
117 }
118
119 /// Allocate all witnesses and return
120 fn alloc_witness<CS: ConstraintSystem<<G as Group>::Base>>(
121 &self,
122 mut cs: CS,
123 ) -> Result<
124 (
125 AllocatedNum<G::Base>,
126 AllocatedNum<G::Base>,
127 AllocatedNum<G::Base>,
128 AllocatedNum<G::Base>,
129 AllocatedRelaxedR1CSInstance<G>,
130 AllocatedR1CSInstance<G>,
131 AllocatedPoint<G::Base>,
132 ),
133 SynthesisError,
134 > {
135 // Allocate the params
136 let params = alloc_scalar_as_base::<G, _>(
137 cs.namespace(|| "params"),
138 self.inputs.get().map_or(None, |inputs| Some(inputs.params)),
139 )?;
140
141 // Allocate i
142 let i = AllocatedNum::alloc(cs.namespace(|| "i"), || Ok(self.inputs.get()?.i))?;
143
144 // Allocate z0
145 let z_0 = AllocatedNum::alloc(cs.namespace(|| "z0"), || Ok(self.inputs.get()?.z0))?;
146
147 // Allocate zi. If inputs.zi is not provided (base case) allocate default value 0
148 let z_i = AllocatedNum::alloc(cs.namespace(|| "zi"), || {
149 Ok(self.inputs.get()?.zi.unwrap_or_else(G::Base::zero))
150 })?;
151
152 // Allocate the running instance
153 let U: AllocatedRelaxedR1CSInstance<G> = AllocatedRelaxedR1CSInstance::alloc(
154 cs.namespace(|| "Allocate U"),
155 self.inputs.get().map_or(None, |inputs| {
156 inputs.U.get().map_or(None, |U| Some(U.clone()))
157 }),
158 self.params.limb_width,
159 self.params.n_limbs,
160 )?;
161
162 // Allocate the instance to be folded in
163 let u = AllocatedR1CSInstance::alloc(
164 cs.namespace(|| "allocate instance u to fold"),
165 self.inputs.get().map_or(None, |inputs| {
166 inputs.u.get().map_or(None, |u| Some(u.clone()))
167 }),
168 )?;
169
170 // Allocate T
171 let T = AllocatedPoint::alloc(
172 cs.namespace(|| "allocate T"),
173 self.inputs.get().map_or(None, |inputs| {
174 inputs
175 .T
176 .get()
177 .map_or(None, |T| Some(T.comm.to_coordinates()))
178 }),
179 )?;
180
181 Ok((params, i, z_0, z_i, U, u, T))
182 }
183
184 /// Synthesizes base case and returns the new relaxed R1CSInstance
185 fn synthesize_base_case<CS: ConstraintSystem<<G as Group>::Base>>(
186 &self,
187 mut cs: CS,
188 u: AllocatedR1CSInstance<G>,
189 ) -> Result<AllocatedRelaxedR1CSInstance<G>, SynthesisError> {
190 let U_default: AllocatedRelaxedR1CSInstance<G> = if self.params.is_primary_circuit {
191 // The primary circuit just returns the default R1CS instance
192 AllocatedRelaxedR1CSInstance::default(
193 cs.namespace(|| "Allocate U_default"),
194 self.params.limb_width,
195 self.params.n_limbs,
196 )?
197 } else {
198 // The secondary circuit returns the incoming R1CS instance
199 AllocatedRelaxedR1CSInstance::from_r1cs_instance(
200 cs.namespace(|| "Allocate U_default"),
201 u,
202 self.params.limb_width,
203 self.params.n_limbs,
204 )?
205 };
206 Ok(U_default)
207 }
208
209 /// Synthesizes non base case and returns the new relaxed R1CSInstance
210 /// And a boolean indicating if all checks pass
211 #[allow(clippy::too_many_arguments)]
212 fn synthesize_non_base_case<CS: ConstraintSystem<<G as Group>::Base>>(
213 &self,
214 mut cs: CS,
215 params: AllocatedNum<G::Base>,
216 i: AllocatedNum<G::Base>,
217 z_0: AllocatedNum<G::Base>,
218 z_i: AllocatedNum<G::Base>,
219 U: AllocatedRelaxedR1CSInstance<G>,
220 u: AllocatedR1CSInstance<G>,
221 T: AllocatedPoint<G::Base>,
222 ) -> Result<(AllocatedRelaxedR1CSInstance<G>, AllocatedBit), SynthesisError> {
223 // Check that u.x[0] = Hash(params, U, i, z0, zi)
224 let mut ro: PoseidonROGadget<G::Base> = PoseidonROGadget::new(self.ro_consts.clone());
225 ro.absorb(params.clone());
226 ro.absorb(i);
227 ro.absorb(z_0);
228 ro.absorb(z_i);
229 let _ = U.absorb_in_ro(cs.namespace(|| "absorb U"), &mut ro)?;
230
231 let hash_bits = ro.get_hash(cs.namespace(|| "Input hash"))?;
232 let hash = le_bits_to_num(cs.namespace(|| "bits to hash"), hash_bits)?;
233 let check_pass = alloc_num_equals(
234 cs.namespace(|| "check consistency of u.X[0] with H(params, U, i, z0, zi)"),
235 &u.X0,
236 &hash,
237 )?;
238
239 // Run NIFS Verifier
240 let U_fold = U.fold_with_r1cs(
241 cs.namespace(|| "compute fold of U and u"),
242 params,
243 u,
244 T,
245 self.ro_consts.clone(),
246 self.params.limb_width,
247 self.params.n_limbs,
248 )?;
249
250 Ok((U_fold, check_pass))
251 }
252}
253
254impl<G, SC> Circuit<<G as Group>::Base> for NIFSVerifierCircuit<G, SC>
255where
256 G: Group,
257 SC: StepCircuit<G::Base>,
258{
259 fn synthesize<CS: ConstraintSystem<<G as Group>::Base>>(
260 self,
261 cs: &mut CS,
262 ) -> Result<(), SynthesisError> {
263 // Allocate all witnesses
264 let (params, i, z_0, z_i, U, u, T) =
265 self.alloc_witness(cs.namespace(|| "allocate the circuit witness"))?;
266
267 // Compute variable indicating if this is the base case
268 let zero = alloc_zero(cs.namespace(|| "zero"))?;
269 let is_base_case = alloc_num_equals(cs.namespace(|| "Check if base case"), &i.clone(), &zero)?;
270
271 // Synthesize the circuit for the base case and get the new running instance
272 let Unew_base = self.synthesize_base_case(cs.namespace(|| "base case"), u.clone())?;
273
274 // Synthesize the circuit for the non-base case and get the new running
275 // instance along with a boolean indicating if all checks have passed
276 let (Unew_non_base, check_non_base_pass) = self.synthesize_non_base_case(
277 cs.namespace(|| "synthesize non base case"),
278 params.clone(),
279 i.clone(),
280 z_0.clone(),
281 z_i.clone(),
282 U,
283 u.clone(),
284 T,
285 )?;
286
287 // Either check_non_base_pass=true or we are in the base case
288 let should_be_false = AllocatedBit::nor(
289 cs.namespace(|| "check_non_base_pass nor base_case"),
290 &check_non_base_pass,
291 &is_base_case,
292 )?;
293 cs.enforce(
294 || "check_non_base_pass nor base_case = false",
295 |lc| lc + should_be_false.get_variable(),
296 |lc| lc + CS::one(),
297 |lc| lc,
298 );
299
300 // Compute the U_new
301 let Unew = Unew_base.conditionally_select(
302 cs.namespace(|| "compute U_new"),
303 Unew_non_base,
304 &Boolean::from(is_base_case.clone()),
305 )?;
306
307 // Compute i + 1
308 let i_new = AllocatedNum::alloc(cs.namespace(|| "i + 1"), || {
309 Ok(*i.get_value().get()? + G::Base::one())
310 })?;
311 cs.enforce(
312 || "check i + 1",
313 |lc| lc,
314 |lc| lc,
315 |lc| lc + i_new.get_variable() - CS::one() - i.get_variable(),
316 );
317
318 // Compute z_{i+1}
319 let z_input = conditionally_select(
320 cs.namespace(|| "select input to F"),
321 &z_0,
322 &z_i,
323 &Boolean::from(is_base_case),
324 )?;
325
326 let z_next = self
327 .step_circuit
328 .synthesize(&mut cs.namespace(|| "F"), z_input)?;
329
330 // Compute the new hash H(params, Unew, i+1, z0, z_{i+1})
331 let mut ro: PoseidonROGadget<G::Base> = PoseidonROGadget::new(self.ro_consts);
332 ro.absorb(params);
333 ro.absorb(i_new.clone());
334 ro.absorb(z_0);
335 ro.absorb(z_next);
336 let _ = Unew.absorb_in_ro(cs.namespace(|| "absorb U_new"), &mut ro)?;
337 let hash_bits = ro.get_hash(cs.namespace(|| "output hash bits"))?;
338 let hash = le_bits_to_num(cs.namespace(|| "convert hash to num"), hash_bits)?;
339
340 // Outputs the computed hash and u.X[1] that corresponds to the hash of the other circuit
341 let _ = u
342 .X1
343 .inputize(cs.namespace(|| "Output unmodified hash of the other circuit"))?;
344 let _ = hash.inputize(cs.namespace(|| "output new hash of this circuit"))?;
345
346 Ok(())
347 }
348}
349
350#[cfg(test)]
351mod tests {
352 use super::*;
353 use crate::bellperson::{shape_cs::ShapeCS, solver::SatisfyingAssignment};
354 type G1 = pasta_curves::pallas::Point;
355 type G2 = pasta_curves::vesta::Point;
356 use crate::constants::{BN_LIMB_WIDTH, BN_N_LIMBS};
357 use crate::{
358 bellperson::r1cs::{NovaShape, NovaWitness},
359 traits::HashFuncConstantsTrait,
360 };
361 use ff::PrimeField;
362 use std::marker::PhantomData;
363
364 #[derive(Clone)]
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 assert_eq!(cs.num_constraints(), 20584);
408
409 // Initialize the shape and gens for the secondary
410 let circuit2: NIFSVerifierCircuit<G1, TestCircuit<<G1 as Group>::Base>> =
411 NIFSVerifierCircuit::new(
412 params2.clone(),
413 None,
414 TestCircuit {
415 _p: Default::default(),
416 },
417 ro_consts2.clone(),
418 );
419 let mut cs: ShapeCS<G2> = ShapeCS::new();
420 let _ = circuit2.synthesize(&mut cs);
421 let (shape2, gens2) = (cs.r1cs_shape(), cs.r1cs_gens());
422 assert_eq!(cs.num_constraints(), 21124);
423
424 // Execute the base case for the primary
425 let zero1 = <<G2 as Group>::Base as Field>::zero();
426 let mut cs1: SatisfyingAssignment<G1> = SatisfyingAssignment::new();
427 let inputs1: NIFSVerifierCircuitInputs<G2> =
428 NIFSVerifierCircuitInputs::new(shape2.get_digest(), zero1, zero1, None, None, None, None);
429 let circuit1: NIFSVerifierCircuit<G2, TestCircuit<<G2 as Group>::Base>> =
430 NIFSVerifierCircuit::new(
431 params1,
432 Some(inputs1),
433 TestCircuit {
434 _p: Default::default(),
435 },
436 ro_consts1,
437 );
438 let _ = circuit1.synthesize(&mut cs1);
439 let (inst1, witness1) = cs1.r1cs_instance_and_witness(&shape1, &gens1).unwrap();
440 // Make sure that this is satisfiable
441 assert!(shape1.is_sat(&gens1, &inst1, &witness1).is_ok());
442
443 // Execute the base case for the secondary
444 let zero2 = <<G1 as Group>::Base as Field>::zero();
445 let mut cs2: SatisfyingAssignment<G2> = SatisfyingAssignment::new();
446 let inputs2: NIFSVerifierCircuitInputs<G1> = NIFSVerifierCircuitInputs::new(
447 shape1.get_digest(),
448 zero2,
449 zero2,
450 None,
451 None,
452 Some(inst1),
453 None,
454 );
455 let circuit: NIFSVerifierCircuit<G1, TestCircuit<<G1 as Group>::Base>> =
456 NIFSVerifierCircuit::new(
457 params2,
458 Some(inputs2),
459 TestCircuit {
460 _p: Default::default(),
461 },
462 ro_consts2,
463 );
464 let _ = circuit.synthesize(&mut cs2);
465 let (inst2, witness2) = cs2.r1cs_instance_and_witness(&shape2, &gens2).unwrap();
466 // Make sure that it is satisfiable
467 assert!(shape2.is_sat(&gens2, &inst2, &witness2).is_ok());
468 }
469}