sonobe/folding-schemes/src/folding/nova/circuits.rs
folding-schemes/src/folding/nova/circuits.rsRaw
1/// contains [Nova](https://eprint.iacr.org/2021/370.pdf) related circuits
2use ark_crypto_primitives::sponge::{
3 constraints::{AbsorbGadget, CryptographicSpongeVar},
4 poseidon::{constraints::PoseidonSpongeVar, PoseidonConfig},
5 Absorb, CryptographicSponge,
6};
7use ark_ec::{CurveGroup, Group};
8use ark_ff::PrimeField;
9use ark_r1cs_std::{
10 alloc::{AllocVar, AllocationMode},
11 boolean::Boolean,
12 eq::EqGadget,
13 fields::{fp::FpVar, FieldVar},
14 groups::GroupOpsBounds,
15 prelude::CurveVar,
16 uint8::UInt8,
17 R1CSVar, ToConstraintFieldGadget,
18};
19use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystemRef, Namespace, SynthesisError};
20use ark_std::{fmt::Debug, One, Zero};
21use core::{borrow::Borrow, marker::PhantomData};
22
23use super::CommittedInstance;
24use crate::constants::N_BITS_RO;
25use crate::folding::circuits::{
26 cyclefold::{
27 CycleFoldChallengeGadget, CycleFoldCommittedInstanceVar, NIFSFullGadget, CF_IO_LEN,
28 },
29 nonnative::{affine::NonNativeAffineVar, uint::NonNativeUintVar},
30 CF1, CF2,
31};
32use crate::frontend::FCircuit;
33use crate::transcript::{AbsorbNonNativeGadget, Transcript, TranscriptVar};
34
35/// CommittedInstanceVar contains the u, x, cmE and cmW values which are folded on the main Nova
36/// constraints field (E1::Fr, where E1 is the main curve). The peculiarity is that cmE and cmW are
37/// represented non-natively over the constraint field.
38#[derive(Debug, Clone)]
39pub struct CommittedInstanceVar<C: CurveGroup>
40where
41 <C as ark_ec::CurveGroup>::BaseField: ark_ff::PrimeField,
42{
43 pub u: FpVar<C::ScalarField>,
44 pub x: Vec<FpVar<C::ScalarField>>,
45 pub cmE: NonNativeAffineVar<C>,
46 pub cmW: NonNativeAffineVar<C>,
47}
48
49impl<C> AllocVar<CommittedInstance<C>, CF1<C>> for CommittedInstanceVar<C>
50where
51 C: CurveGroup,
52 <C as ark_ec::CurveGroup>::BaseField: PrimeField,
53{
54 fn new_variable<T: Borrow<CommittedInstance<C>>>(
55 cs: impl Into<Namespace<CF1<C>>>,
56 f: impl FnOnce() -> Result<T, SynthesisError>,
57 mode: AllocationMode,
58 ) -> Result<Self, SynthesisError> {
59 f().and_then(|val| {
60 let cs = cs.into();
61
62 let u = FpVar::<C::ScalarField>::new_variable(cs.clone(), || Ok(val.borrow().u), mode)?;
63 let x: Vec<FpVar<C::ScalarField>> =
64 Vec::new_variable(cs.clone(), || Ok(val.borrow().x.clone()), mode)?;
65
66 let cmE =
67 NonNativeAffineVar::<C>::new_variable(cs.clone(), || Ok(val.borrow().cmE), mode)?;
68 let cmW =
69 NonNativeAffineVar::<C>::new_variable(cs.clone(), || Ok(val.borrow().cmW), mode)?;
70
71 Ok(Self { u, x, cmE, cmW })
72 })
73 }
74}
75
76impl<C> AbsorbGadget<C::ScalarField> for CommittedInstanceVar<C>
77where
78 C: CurveGroup,
79 <C as ark_ec::CurveGroup>::BaseField: ark_ff::PrimeField,
80{
81 fn to_sponge_bytes(&self) -> Result<Vec<UInt8<C::ScalarField>>, SynthesisError> {
82 unimplemented!()
83 }
84
85 fn to_sponge_field_elements(&self) -> Result<Vec<FpVar<C::ScalarField>>, SynthesisError> {
86 Ok([
87 vec![self.u.clone()],
88 self.x.clone(),
89 self.cmE.to_constraint_field()?,
90 self.cmW.to_constraint_field()?,
91 ]
92 .concat())
93 }
94}
95
96impl<C> CommittedInstanceVar<C>
97where
98 C: CurveGroup,
99 <C as Group>::ScalarField: Absorb,
100 <C as ark_ec::CurveGroup>::BaseField: ark_ff::PrimeField,
101{
102 /// hash implements the committed instance hash compatible with the native implementation from
103 /// CommittedInstance.hash.
104 /// Returns `H(i, z_0, z_i, U_i)`, where `i` can be `i` but also `i+1`, and `U` is the
105 /// `CommittedInstance`.
106 /// Additionally it returns the vector of the field elements from the self parameters, so they
107 /// can be reused in other gadgets avoiding recalculating (reconstraining) them.
108 #[allow(clippy::type_complexity)]
109 pub fn hash<S: CryptographicSponge, T: TranscriptVar<CF1<C>, S>>(
110 self,
111 sponge: &T,
112 pp_hash: FpVar<CF1<C>>,
113 i: FpVar<CF1<C>>,
114 z_0: Vec<FpVar<CF1<C>>>,
115 z_i: Vec<FpVar<CF1<C>>>,
116 ) -> Result<(FpVar<CF1<C>>, Vec<FpVar<CF1<C>>>), SynthesisError> {
117 let mut sponge = sponge.clone();
118 let U_vec = self.to_sponge_field_elements()?;
119 sponge.absorb(&pp_hash)?;
120 sponge.absorb(&i)?;
121 sponge.absorb(&z_0)?;
122 sponge.absorb(&z_i)?;
123 sponge.absorb(&U_vec)?;
124 Ok((sponge.squeeze_field_elements(1)?.pop().unwrap(), U_vec))
125 }
126}
127
128/// Implements the circuit that does the checks of the Non-Interactive Folding Scheme Verifier
129/// described in section 4 of [Nova](https://eprint.iacr.org/2021/370.pdf), where the cmE & cmW checks are
130/// delegated to the NIFSCycleFoldGadget.
131pub struct NIFSGadget<C: CurveGroup> {
132 _c: PhantomData<C>,
133}
134
135impl<C: CurveGroup> NIFSGadget<C>
136where
137 C: CurveGroup,
138 <C as ark_ec::CurveGroup>::BaseField: ark_ff::PrimeField,
139{
140 pub fn fold_committed_instance(
141 r: FpVar<CF1<C>>,
142 ci1: CommittedInstanceVar<C>, // U_i
143 ci2: CommittedInstanceVar<C>, // u_i
144 ) -> Result<CommittedInstanceVar<C>, SynthesisError> {
145 Ok(CommittedInstanceVar {
146 cmE: NonNativeAffineVar::new_constant(ConstraintSystemRef::None, C::zero())?,
147 cmW: NonNativeAffineVar::new_constant(ConstraintSystemRef::None, C::zero())?,
148 // ci3.u = ci1.u + r * ci2.u
149 u: ci1.u + &r * ci2.u,
150 // ci3.x = ci1.x + r * ci2.x
151 x: ci1
152 .x
153 .iter()
154 .zip(ci2.x)
155 .map(|(a, b)| a + &r * &b)
156 .collect::<Vec<FpVar<CF1<C>>>>(),
157 })
158 }
159
160 /// Implements the constraints for NIFS.V for u and x, since cm(E) and cm(W) are delegated to
161 /// the CycleFold circuit.
162 pub fn verify(
163 r: FpVar<CF1<C>>,
164 ci1: CommittedInstanceVar<C>, // U_i
165 ci2: CommittedInstanceVar<C>, // u_i
166 ci3: CommittedInstanceVar<C>, // U_{i+1}
167 ) -> Result<(), SynthesisError> {
168 let ci = Self::fold_committed_instance(r, ci1, ci2)?;
169
170 ci.u.enforce_equal(&ci3.u)?;
171 ci.x.enforce_equal(&ci3.x)?;
172
173 Ok(())
174 }
175}
176
177/// ChallengeGadget computes the RO challenge used for the Nova instances NIFS, it contains a
178/// rust-native and a in-circuit compatible versions.
179pub struct ChallengeGadget<C: CurveGroup> {
180 _c: PhantomData<C>,
181}
182impl<C: CurveGroup> ChallengeGadget<C>
183where
184 C: CurveGroup,
185 <C as CurveGroup>::BaseField: PrimeField,
186 <C as Group>::ScalarField: Absorb,
187{
188 pub fn get_challenge_native<T: Transcript<C::ScalarField>>(
189 transcript: &mut T,
190 pp_hash: C::ScalarField, // public params hash
191 U_i: CommittedInstance<C>,
192 u_i: CommittedInstance<C>,
193 cmT: C,
194 ) -> Vec<bool> {
195 transcript.absorb(&pp_hash);
196 transcript.absorb(&U_i);
197 transcript.absorb(&u_i);
198 transcript.absorb_nonnative(&cmT);
199 transcript.squeeze_bits(N_BITS_RO)
200 }
201
202 // compatible with the native get_challenge_native
203 pub fn get_challenge_gadget<S: CryptographicSponge, T: TranscriptVar<CF1<C>, S>>(
204 transcript: &mut T,
205 pp_hash: FpVar<CF1<C>>, // public params hash
206 U_i_vec: Vec<FpVar<CF1<C>>>, // apready processed input, so we don't have to recompute these values
207 u_i: CommittedInstanceVar<C>,
208 cmT: NonNativeAffineVar<C>,
209 ) -> Result<Vec<Boolean<C::ScalarField>>, SynthesisError> {
210 transcript.absorb(&pp_hash)?;
211 transcript.absorb(&U_i_vec)?;
212 transcript.absorb(&u_i)?;
213 transcript.absorb_nonnative(&cmT)?;
214 transcript.squeeze_bits(N_BITS_RO)
215 }
216}
217
218/// AugmentedFCircuit implements the F' circuit (augmented F) defined in
219/// [Nova](https://eprint.iacr.org/2021/370.pdf) together with the extra constraints defined in
220/// [CycleFold](https://eprint.iacr.org/2023/1192.pdf).
221#[derive(Debug, Clone)]
222pub struct AugmentedFCircuit<
223 C1: CurveGroup,
224 C2: CurveGroup,
225 GC2: CurveVar<C2, CF2<C2>>,
226 FC: FCircuit<CF1<C1>>,
227> where
228 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
229{
230 pub _gc2: PhantomData<GC2>,
231 pub poseidon_config: PoseidonConfig<CF1<C1>>,
232 pub pp_hash: Option<CF1<C1>>,
233 pub i: Option<CF1<C1>>,
234 pub i_usize: Option<usize>,
235 pub z_0: Option<Vec<C1::ScalarField>>,
236 pub z_i: Option<Vec<C1::ScalarField>>,
237 pub external_inputs: Option<Vec<C1::ScalarField>>,
238 pub u_i_cmW: Option<C1>,
239 pub U_i: Option<CommittedInstance<C1>>,
240 pub U_i1_cmE: Option<C1>,
241 pub U_i1_cmW: Option<C1>,
242 pub cmT: Option<C1>,
243 pub F: FC, // F circuit
244 pub x: Option<CF1<C1>>, // public input (u_{i+1}.x[0])
245
246 // cyclefold verifier on C1
247 // Here 'cf1, cf2' are for each of the CycleFold circuits, corresponding to the fold of cmW and
248 // cmE respectively
249 pub cf1_u_i_cmW: Option<C2>, // input
250 pub cf2_u_i_cmW: Option<C2>, // input
251 pub cf_U_i: Option<CommittedInstance<C2>>, // input
252 pub cf1_cmT: Option<C2>,
253 pub cf2_cmT: Option<C2>,
254 pub cf_x: Option<CF1<C1>>, // public input (u_{i+1}.x[1])
255}
256
257impl<C1: CurveGroup, C2: CurveGroup, GC2: CurveVar<C2, CF2<C2>>, FC: FCircuit<CF1<C1>>>
258 AugmentedFCircuit<C1, C2, GC2, FC>
259where
260 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
261{
262 pub fn empty(poseidon_config: &PoseidonConfig<CF1<C1>>, F_circuit: FC) -> Self {
263 Self {
264 _gc2: PhantomData,
265 poseidon_config: poseidon_config.clone(),
266 pp_hash: None,
267 i: None,
268 i_usize: None,
269 z_0: None,
270 z_i: None,
271 external_inputs: None,
272 u_i_cmW: None,
273 U_i: None,
274 U_i1_cmE: None,
275 U_i1_cmW: None,
276 cmT: None,
277 F: F_circuit,
278 x: None,
279 // cyclefold values
280 cf1_u_i_cmW: None,
281 cf2_u_i_cmW: None,
282 cf_U_i: None,
283 cf1_cmT: None,
284 cf2_cmT: None,
285 cf_x: None,
286 }
287 }
288}
289
290impl<C1, C2, GC2, FC> ConstraintSynthesizer<CF1<C1>> for AugmentedFCircuit<C1, C2, GC2, FC>
291where
292 C1: CurveGroup,
293 C2: CurveGroup,
294 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
295 FC: FCircuit<CF1<C1>>,
296 <C1 as CurveGroup>::BaseField: PrimeField,
297 <C2 as CurveGroup>::BaseField: PrimeField,
298 <C1 as Group>::ScalarField: Absorb,
299 <C2 as Group>::ScalarField: Absorb,
300 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
301 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
302{
303 fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C1>>) -> Result<(), SynthesisError> {
304 let pp_hash = FpVar::<CF1<C1>>::new_witness(cs.clone(), || {
305 Ok(self.pp_hash.unwrap_or_else(CF1::<C1>::zero))
306 })?;
307 let i = FpVar::<CF1<C1>>::new_witness(cs.clone(), || {
308 Ok(self.i.unwrap_or_else(CF1::<C1>::zero))
309 })?;
310 let z_0 = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
311 Ok(self
312 .z_0
313 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
314 })?;
315 let z_i = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
316 Ok(self
317 .z_i
318 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
319 })?;
320 let external_inputs = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
321 Ok(self
322 .external_inputs
323 .unwrap_or(vec![CF1::<C1>::zero(); self.F.external_inputs_len()]))
324 })?;
325
326 let u_dummy = CommittedInstance::dummy(2);
327 let U_i = CommittedInstanceVar::<C1>::new_witness(cs.clone(), || {
328 Ok(self.U_i.unwrap_or(u_dummy.clone()))
329 })?;
330 let U_i1_cmE = NonNativeAffineVar::new_witness(cs.clone(), || {
331 Ok(self.U_i1_cmE.unwrap_or_else(C1::zero))
332 })?;
333 let U_i1_cmW = NonNativeAffineVar::new_witness(cs.clone(), || {
334 Ok(self.U_i1_cmW.unwrap_or_else(C1::zero))
335 })?;
336
337 let cmT =
338 NonNativeAffineVar::new_witness(cs.clone(), || Ok(self.cmT.unwrap_or_else(C1::zero)))?;
339
340 let cf_u_dummy = CommittedInstance::dummy(CF_IO_LEN);
341 let cf_U_i = CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || {
342 Ok(self.cf_U_i.unwrap_or(cf_u_dummy.clone()))
343 })?;
344 let cf1_cmT = GC2::new_witness(cs.clone(), || Ok(self.cf1_cmT.unwrap_or_else(C2::zero)))?;
345 let cf2_cmT = GC2::new_witness(cs.clone(), || Ok(self.cf2_cmT.unwrap_or_else(C2::zero)))?;
346
347 // `sponge` is for digest computation.
348 let sponge = PoseidonSpongeVar::<C1::ScalarField>::new(cs.clone(), &self.poseidon_config);
349 // `transcript` is for challenge generation.
350 let mut transcript = sponge.clone();
351
352 // get z_{i+1} from the F circuit
353 let i_usize = self.i_usize.unwrap_or(0);
354 let z_i1 =
355 self.F
356 .generate_step_constraints(cs.clone(), i_usize, z_i.clone(), external_inputs)?;
357
358 let is_basecase = i.is_zero()?;
359
360 // Primary Part
361 // P.1. Compute u_i.x
362 // u_i.x[0] = H(i, z_0, z_i, U_i)
363 let (u_i_x, U_i_vec) = U_i.clone().hash(
364 &sponge,
365 pp_hash.clone(),
366 i.clone(),
367 z_0.clone(),
368 z_i.clone(),
369 )?;
370 // u_i.x[1] = H(cf_U_i)
371 let (cf_u_i_x, cf_U_i_vec) = cf_U_i.clone().hash(&sponge, pp_hash.clone())?;
372
373 // P.2. Construct u_i
374 let u_i = CommittedInstanceVar {
375 // u_i.cmE = cm(0)
376 cmE: NonNativeAffineVar::new_constant(cs.clone(), C1::zero())?,
377 // u_i.u = 1
378 u: FpVar::one(),
379 // u_i.cmW is provided by the prover as witness
380 cmW: NonNativeAffineVar::new_witness(cs.clone(), || {
381 Ok(self.u_i_cmW.unwrap_or(C1::zero()))
382 })?,
383 // u_i.x is computed in step 1
384 x: vec![u_i_x, cf_u_i_x],
385 };
386
387 // P.3. nifs.verify, obtains U_{i+1} by folding u_i & U_i .
388
389 // compute r = H(u_i, U_i, cmT)
390 let r_bits = ChallengeGadget::<C1>::get_challenge_gadget(
391 &mut transcript,
392 pp_hash.clone(),
393 U_i_vec,
394 u_i.clone(),
395 cmT.clone(),
396 )?;
397 let r = Boolean::le_bits_to_fp_var(&r_bits)?;
398 // Also convert r_bits to a `NonNativeFieldVar`
399 let r_nonnat = {
400 let mut bits = r_bits;
401 bits.resize(C1::BaseField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
402 NonNativeUintVar::from(&bits)
403 };
404
405 // Notice that NIFSGadget::fold_committed_instance does not fold cmE & cmW.
406 // We set `U_i1.cmE` and `U_i1.cmW` to unconstrained witnesses `U_i1_cmE` and `U_i1_cmW`
407 // respectively.
408 // The correctness of them will be checked on the other curve.
409 let mut U_i1 = NIFSGadget::<C1>::fold_committed_instance(r, U_i.clone(), u_i.clone())?;
410 U_i1.cmE = U_i1_cmE;
411 U_i1.cmW = U_i1_cmW;
412
413 // P.4.a compute and check the first output of F'
414 // Base case: u_{i+1}.x[0] == H((i+1, z_0, z_{i+1}, U_{\bot})
415 // Non-base case: u_{i+1}.x[0] == H((i+1, z_0, z_{i+1}, U_{i+1})
416 let (u_i1_x, _) = U_i1.clone().hash(
417 &sponge,
418 pp_hash.clone(),
419 i + FpVar::<CF1<C1>>::one(),
420 z_0.clone(),
421 z_i1.clone(),
422 )?;
423 let (u_i1_x_base, _) = CommittedInstanceVar::new_constant(cs.clone(), u_dummy)?.hash(
424 &sponge,
425 pp_hash.clone(),
426 FpVar::<CF1<C1>>::one(),
427 z_0.clone(),
428 z_i1.clone(),
429 )?;
430 let x = FpVar::new_input(cs.clone(), || Ok(self.x.unwrap_or(u_i1_x_base.value()?)))?;
431 x.enforce_equal(&is_basecase.select(&u_i1_x_base, &u_i1_x)?)?;
432
433 // CycleFold part
434 // C.1. Compute cf1_u_i.x and cf2_u_i.x
435 let cfW_x = vec![
436 r_nonnat.clone(),
437 U_i.cmW.x,
438 U_i.cmW.y,
439 u_i.cmW.x,
440 u_i.cmW.y,
441 U_i1.cmW.x,
442 U_i1.cmW.y,
443 ];
444 let cfE_x = vec![
445 r_nonnat, U_i.cmE.x, U_i.cmE.y, cmT.x, cmT.y, U_i1.cmE.x, U_i1.cmE.y,
446 ];
447
448 // ensure that cf1_u & cf2_u have as public inputs the cmW & cmE from main instances U_i,
449 // u_i, U_i+1 coordinates of the commitments
450 // C.2. Construct `cf1_u_i` and `cf2_u_i`
451 let cf1_u_i = CycleFoldCommittedInstanceVar {
452 // cf1_u_i.cmE = 0
453 cmE: GC2::zero(),
454 // cf1_u_i.u = 1
455 u: NonNativeUintVar::new_constant(cs.clone(), C1::BaseField::one())?,
456 // cf1_u_i.cmW is provided by the prover as witness
457 cmW: GC2::new_witness(cs.clone(), || Ok(self.cf1_u_i_cmW.unwrap_or(C2::zero())))?,
458 // cf1_u_i.x is computed in step 1
459 x: cfW_x,
460 };
461 let cf2_u_i = CycleFoldCommittedInstanceVar {
462 // cf2_u_i.cmE = 0
463 cmE: GC2::zero(),
464 // cf2_u_i.u = 1
465 u: NonNativeUintVar::new_constant(cs.clone(), C1::BaseField::one())?,
466 // cf2_u_i.cmW is provided by the prover as witness
467 cmW: GC2::new_witness(cs.clone(), || Ok(self.cf2_u_i_cmW.unwrap_or(C2::zero())))?,
468 // cf2_u_i.x is computed in step 1
469 x: cfE_x,
470 };
471
472 // C.3. nifs.verify, obtains cf1_U_{i+1} by folding cf1_u_i & cf_U_i, and then cf_U_{i+1}
473 // by folding cf2_u_i & cf1_U_{i+1}.
474
475 // compute cf1_r = H(cf1_u_i, cf_U_i, cf1_cmT)
476 // cf_r_bits is denoted by rho* in the paper.
477 let cf1_r_bits = CycleFoldChallengeGadget::<C2, GC2>::get_challenge_gadget(
478 &mut transcript,
479 pp_hash.clone(),
480 cf_U_i_vec,
481 cf1_u_i.clone(),
482 cf1_cmT.clone(),
483 )?;
484 // Convert cf1_r_bits to a `NonNativeFieldVar`
485 let cf1_r_nonnat = {
486 let mut bits = cf1_r_bits.clone();
487 bits.resize(C1::BaseField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
488 NonNativeUintVar::from(&bits)
489 };
490 // Fold cf1_u_i & cf_U_i into cf1_U_{i+1}
491 let cf1_U_i1 = NIFSFullGadget::<C2, GC2>::fold_committed_instance(
492 cf1_r_bits,
493 cf1_r_nonnat,
494 cf1_cmT,
495 cf_U_i,
496 cf1_u_i,
497 )?;
498
499 // same for cf2_r:
500 let cf2_r_bits = CycleFoldChallengeGadget::<C2, GC2>::get_challenge_gadget(
501 &mut transcript,
502 pp_hash.clone(),
503 cf1_U_i1.to_native_sponge_field_elements()?,
504 cf2_u_i.clone(),
505 cf2_cmT.clone(),
506 )?;
507 let cf2_r_nonnat = {
508 let mut bits = cf2_r_bits.clone();
509 bits.resize(C1::BaseField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
510 NonNativeUintVar::from(&bits)
511 };
512 let cf_U_i1 = NIFSFullGadget::<C2, GC2>::fold_committed_instance(
513 cf2_r_bits,
514 cf2_r_nonnat,
515 cf2_cmT,
516 cf1_U_i1, // the output from NIFS.V(cf1_r, cf_U, cfE_u)
517 cf2_u_i,
518 )?;
519
520 // Back to Primary Part
521 // P.4.b compute and check the second output of F'
522 // Base case: u_{i+1}.x[1] == H(cf_U_{\bot})
523 // Non-base case: u_{i+1}.x[1] == H(cf_U_{i+1})
524 let (cf_u_i1_x, _) = cf_U_i1.clone().hash(&sponge, pp_hash.clone())?;
525 let (cf_u_i1_x_base, _) =
526 CycleFoldCommittedInstanceVar::new_constant(cs.clone(), cf_u_dummy)?
527 .hash(&sponge, pp_hash)?;
528 let cf_x = FpVar::new_input(cs.clone(), || {
529 Ok(self.cf_x.unwrap_or(cf_u_i1_x_base.value()?))
530 })?;
531 cf_x.enforce_equal(&is_basecase.select(&cf_u_i1_x_base, &cf_u_i1_x)?)?;
532
533 Ok(())
534 }
535}
536
537#[cfg(test)]
538pub mod tests {
539 use super::*;
540 use ark_bn254::{Fr, G1Projective as Projective};
541 use ark_crypto_primitives::sponge::poseidon::PoseidonSponge;
542 use ark_ff::BigInteger;
543 use ark_relations::r1cs::ConstraintSystem;
544 use ark_std::UniformRand;
545
546 use crate::commitment::pedersen::Pedersen;
547 use crate::folding::nova::nifs::tests::prepare_simple_fold_inputs;
548 use crate::folding::nova::nifs::NIFS;
549 use crate::transcript::poseidon::poseidon_canonical_config;
550
551 #[test]
552 fn test_committed_instance_var() {
553 let mut rng = ark_std::test_rng();
554
555 let ci = CommittedInstance::<Projective> {
556 cmE: Projective::rand(&mut rng),
557 u: Fr::rand(&mut rng),
558 cmW: Projective::rand(&mut rng),
559 x: vec![Fr::rand(&mut rng); 1],
560 };
561
562 let cs = ConstraintSystem::<Fr>::new_ref();
563 let ciVar =
564 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci.clone())).unwrap();
565 assert_eq!(ciVar.u.value().unwrap(), ci.u);
566 assert_eq!(ciVar.x.value().unwrap(), ci.x);
567 // the values cmE and cmW are checked in the CycleFold's circuit
568 // CommittedInstanceInCycleFoldVar in
569 // nova::cyclefold::tests::test_committed_instance_cyclefold_var
570 }
571
572 #[test]
573 fn test_nifs_gadget() {
574 let (_, _, _, _, ci1, _, ci2, _, ci3, _, cmT, _, r_Fr) = prepare_simple_fold_inputs();
575
576 let ci3_verifier = NIFS::<Projective, Pedersen<Projective>>::verify(r_Fr, &ci1, &ci2, &cmT);
577 assert_eq!(ci3_verifier, ci3);
578
579 let cs = ConstraintSystem::<Fr>::new_ref();
580
581 let rVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(r_Fr)).unwrap();
582 let ci1Var =
583 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci1.clone()))
584 .unwrap();
585 let ci2Var =
586 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci2.clone()))
587 .unwrap();
588 let ci3Var =
589 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci3.clone()))
590 .unwrap();
591
592 NIFSGadget::<Projective>::verify(
593 rVar.clone(),
594 ci1Var.clone(),
595 ci2Var.clone(),
596 ci3Var.clone(),
597 )
598 .unwrap();
599 assert!(cs.is_satisfied().unwrap());
600 }
601
602 #[test]
603 fn test_committed_instance_hash() {
604 let mut rng = ark_std::test_rng();
605 let poseidon_config = poseidon_canonical_config::<Fr>();
606 let sponge = PoseidonSponge::<Fr>::new(&poseidon_config);
607 let pp_hash = Fr::from(42u32); // only for test
608
609 let i = Fr::from(3_u32);
610 let z_0 = vec![Fr::from(3_u32)];
611 let z_i = vec![Fr::from(3_u32)];
612 let ci = CommittedInstance::<Projective> {
613 cmE: Projective::rand(&mut rng),
614 u: Fr::rand(&mut rng),
615 cmW: Projective::rand(&mut rng),
616 x: vec![Fr::rand(&mut rng); 1],
617 };
618
619 // compute the CommittedInstance hash natively
620 let h = ci.hash(&sponge, pp_hash, i, z_0.clone(), z_i.clone());
621
622 let cs = ConstraintSystem::<Fr>::new_ref();
623
624 let pp_hashVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(pp_hash)).unwrap();
625 let iVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(i)).unwrap();
626 let z_0Var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_0.clone())).unwrap();
627 let z_iVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_i.clone())).unwrap();
628 let ciVar =
629 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci.clone())).unwrap();
630
631 let sponge = PoseidonSpongeVar::<Fr>::new(cs.clone(), &poseidon_config);
632
633 // compute the CommittedInstance hash in-circuit
634 let (hVar, _) = ciVar
635 .hash(&sponge, pp_hashVar, iVar, z_0Var, z_iVar)
636 .unwrap();
637 assert!(cs.is_satisfied().unwrap());
638
639 // check that the natively computed and in-circuit computed hashes match
640 assert_eq!(hVar.value().unwrap(), h);
641 }
642
643 // checks that the gadget and native implementations of the challenge computation match
644 #[test]
645 fn test_challenge_gadget() {
646 let mut rng = ark_std::test_rng();
647 let poseidon_config = poseidon_canonical_config::<Fr>();
648 let mut transcript = PoseidonSponge::<Fr>::new(&poseidon_config);
649
650 let u_i = CommittedInstance::<Projective> {
651 cmE: Projective::rand(&mut rng),
652 u: Fr::rand(&mut rng),
653 cmW: Projective::rand(&mut rng),
654 x: vec![Fr::rand(&mut rng); 1],
655 };
656 let U_i = CommittedInstance::<Projective> {
657 cmE: Projective::rand(&mut rng),
658 u: Fr::rand(&mut rng),
659 cmW: Projective::rand(&mut rng),
660 x: vec![Fr::rand(&mut rng); 1],
661 };
662 let cmT = Projective::rand(&mut rng);
663
664 let pp_hash = Fr::from(42u32); // only for testing
665
666 // compute the challenge natively
667 let r_bits = ChallengeGadget::<Projective>::get_challenge_native(
668 &mut transcript,
669 pp_hash,
670 U_i.clone(),
671 u_i.clone(),
672 cmT,
673 );
674 let r = Fr::from_bigint(BigInteger::from_bits_le(&r_bits)).unwrap();
675
676 let cs = ConstraintSystem::<Fr>::new_ref();
677 let pp_hashVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(pp_hash)).unwrap();
678 let u_iVar =
679 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(u_i.clone()))
680 .unwrap();
681 let U_iVar =
682 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(U_i.clone()))
683 .unwrap();
684 let cmTVar = NonNativeAffineVar::<Projective>::new_witness(cs.clone(), || Ok(cmT)).unwrap();
685 let mut transcriptVar = PoseidonSpongeVar::<Fr>::new(cs.clone(), &poseidon_config);
686
687 // compute the challenge in-circuit
688 let U_iVar_vec = [
689 vec![U_iVar.u.clone()],
690 U_iVar.x.clone(),
691 U_iVar.cmE.to_constraint_field().unwrap(),
692 U_iVar.cmW.to_constraint_field().unwrap(),
693 ]
694 .concat();
695 let r_bitsVar = ChallengeGadget::<Projective>::get_challenge_gadget(
696 &mut transcriptVar,
697 pp_hashVar,
698 U_iVar_vec,
699 u_iVar,
700 cmTVar,
701 )
702 .unwrap();
703 assert!(cs.is_satisfied().unwrap());
704
705 // check that the natively computed and in-circuit computed hashes match
706 let rVar = Boolean::le_bits_to_fp_var(&r_bitsVar).unwrap();
707 assert_eq!(rVar.value().unwrap(), r);
708 assert_eq!(r_bitsVar.value().unwrap(), r_bits);
709 }
710}