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