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