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::{circuit::StepCircuit, Group, HashFuncCircuitTrait, HashFuncConstantsCircuit},
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 NovaAugmentedCircuitParams {
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 NovaAugmentedCircuitParams {
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 NovaAugmentedCircuitInputs<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> NovaAugmentedCircuitInputs<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/// The augmented circuit F' in Nova that includes a step circuit F
87/// and the circuit for the verifier in Nova's non-interactive folding scheme
88pub struct NovaAugmentedCircuit<G, SC>
89where
90 G: Group,
91 SC: StepCircuit<G::Base>,
92{
93 params: NovaAugmentedCircuitParams,
94 ro_consts: HashFuncConstantsCircuit<G>,
95 inputs: Option<NovaAugmentedCircuitInputs<G>>,
96 step_circuit: SC, // The function that is applied for each step
97}
98
99impl<G, SC> NovaAugmentedCircuit<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: NovaAugmentedCircuitParams,
107 inputs: Option<NovaAugmentedCircuitInputs<G>>,
108 step_circuit: SC,
109 ro_consts: HashFuncConstantsCircuit<G>,
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 = G::HashFuncCircuit::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 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 NovaAugmentedCircuit<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 = G::HashFuncCircuit::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 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 u.X1
342 .inputize(cs.namespace(|| "Output unmodified hash of the other circuit"))?;
343 hash.inputize(cs.namespace(|| "output new hash of this circuit"))?;
344
345 Ok(())
346 }
347}
348
349#[cfg(test)]
350mod tests {
351 use super::*;
352 use crate::bellperson::{shape_cs::ShapeCS, solver::SatisfyingAssignment};
353 type G1 = pasta_curves::pallas::Point;
354 type G2 = pasta_curves::vesta::Point;
355 use crate::constants::{BN_LIMB_WIDTH, BN_N_LIMBS};
356 use crate::{
357 bellperson::r1cs::{NovaShape, NovaWitness},
358 poseidon::PoseidonConstantsCircuit,
359 traits::{circuit::TrivialTestCircuit, HashFuncConstantsTrait},
360 };
361
362 #[test]
363 fn test_verification_circuit() {
364 // In the following we use 1 to refer to the primary, and 2 to refer to the secondary circuit
365 let params1 = NovaAugmentedCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS, true);
366 let params2 = NovaAugmentedCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS, false);
367 let ro_consts1: HashFuncConstantsCircuit<G2> = PoseidonConstantsCircuit::new();
368 let ro_consts2: HashFuncConstantsCircuit<G1> = PoseidonConstantsCircuit::new();
369
370 // Initialize the shape and gens for the primary
371 let circuit1: NovaAugmentedCircuit<G2, TrivialTestCircuit<<G2 as Group>::Base>> =
372 NovaAugmentedCircuit::new(
373 params1.clone(),
374 None,
375 TrivialTestCircuit::default(),
376 ro_consts1.clone(),
377 );
378 let mut cs: ShapeCS<G1> = ShapeCS::new();
379 let _ = circuit1.synthesize(&mut cs);
380 let (shape1, gens1) = (cs.r1cs_shape(), cs.r1cs_gens());
381 assert_eq!(cs.num_constraints(), 20584);
382
383 // Initialize the shape and gens for the secondary
384 let circuit2: NovaAugmentedCircuit<G1, TrivialTestCircuit<<G1 as Group>::Base>> =
385 NovaAugmentedCircuit::new(
386 params2.clone(),
387 None,
388 TrivialTestCircuit::default(),
389 ro_consts2.clone(),
390 );
391 let mut cs: ShapeCS<G2> = ShapeCS::new();
392 let _ = circuit2.synthesize(&mut cs);
393 let (shape2, gens2) = (cs.r1cs_shape(), cs.r1cs_gens());
394 assert_eq!(cs.num_constraints(), 21124);
395
396 // Execute the base case for the primary
397 let zero1 = <<G2 as Group>::Base as Field>::zero();
398 let mut cs1: SatisfyingAssignment<G1> = SatisfyingAssignment::new();
399 let inputs1: NovaAugmentedCircuitInputs<G2> =
400 NovaAugmentedCircuitInputs::new(shape2.get_digest(), zero1, zero1, None, None, None, None);
401 let circuit1: NovaAugmentedCircuit<G2, TrivialTestCircuit<<G2 as Group>::Base>> =
402 NovaAugmentedCircuit::new(
403 params1,
404 Some(inputs1),
405 TrivialTestCircuit::default(),
406 ro_consts1,
407 );
408 let _ = circuit1.synthesize(&mut cs1);
409 let (inst1, witness1) = cs1.r1cs_instance_and_witness(&shape1, &gens1).unwrap();
410 // Make sure that this is satisfiable
411 assert!(shape1.is_sat(&gens1, &inst1, &witness1).is_ok());
412
413 // Execute the base case for the secondary
414 let zero2 = <<G1 as Group>::Base as Field>::zero();
415 let mut cs2: SatisfyingAssignment<G2> = SatisfyingAssignment::new();
416 let inputs2: NovaAugmentedCircuitInputs<G1> = NovaAugmentedCircuitInputs::new(
417 shape1.get_digest(),
418 zero2,
419 zero2,
420 None,
421 None,
422 Some(inst1),
423 None,
424 );
425 let circuit: NovaAugmentedCircuit<G1, TrivialTestCircuit<<G1 as Group>::Base>> =
426 NovaAugmentedCircuit::new(
427 params2,
428 Some(inputs2),
429 TrivialTestCircuit::default(),
430 ro_consts2,
431 );
432 let _ = circuit.synthesize(&mut cs2);
433 let (inst2, witness2) = cs2.r1cs_instance_and_witness(&shape2, &gens2).unwrap();
434 // Make sure that it is satisfiable
435 assert!(shape2.is_sat(&gens2, &inst2, &witness2).is_ok());
436 }
437}