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