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::CryptographicSpongeVar,
4 poseidon::{constraints::PoseidonSpongeVar, PoseidonConfig, PoseidonSponge},
5 Absorb,
6};
7use ark_ec::{CurveGroup, Group};
8use ark_ff::PrimeField;
9use ark_r1cs_std::{
10 alloc::AllocVar,
11 boolean::Boolean,
12 eq::EqGadget,
13 fields::{fp::FpVar, FieldVar},
14 prelude::CurveVar,
15 R1CSVar, ToConstraintFieldGadget,
16};
17use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystemRef, SynthesisError};
18use ark_std::{fmt::Debug, One, Zero};
19use core::marker::PhantomData;
20
21use super::{
22 nifs::{
23 nova_circuits::{CommittedInstanceVar, NIFSGadget},
24 NIFSGadgetTrait,
25 },
26 CommittedInstance, NovaCycleFoldConfig,
27};
28use crate::folding::circuits::{
29 cyclefold::{
30 CycleFoldChallengeGadget, CycleFoldCommittedInstance, CycleFoldCommittedInstanceVar,
31 CycleFoldConfig, NIFSFullGadget,
32 },
33 nonnative::{affine::NonNativeAffineVar, uint::NonNativeUintVar},
34 CF1, CF2,
35};
36use crate::folding::traits::{CommittedInstanceVarOps, Dummy};
37use crate::frontend::FCircuit;
38use crate::transcript::AbsorbNonNativeGadget;
39
40/// `AugmentedFCircuit` enhances the original step function `F`, so that it can
41/// be used in recursive arguments such as IVC.
42///
43/// The method for converting `F` to `AugmentedFCircuit` (`F'`) is defined in
44/// [Nova](https://eprint.iacr.org/2021/370.pdf), where `AugmentedFCircuit` not
45/// only invokes `F`, but also adds additional constraints for verifying the
46/// correct folding of primary instances (i.e., Nova's `CommittedInstance`s over
47/// `C1`).
48///
49/// Furthermore, to reduce circuit size over `C2`, we implement the constraints
50/// defined in [CycleFold](https://eprint.iacr.org/2023/1192.pdf). These extra
51/// constraints verify the correct folding of CycleFold instances.
52#[derive(Debug, Clone)]
53pub struct AugmentedFCircuit<
54 C1: CurveGroup,
55 C2: CurveGroup,
56 GC2: CurveVar<C2, CF2<C2>>,
57 FC: FCircuit<CF1<C1>>,
58> {
59 pub(super) _gc2: PhantomData<GC2>,
60 pub(super) poseidon_config: PoseidonConfig<CF1<C1>>,
61 pub(super) pp_hash: Option<CF1<C1>>,
62 pub(super) i: Option<CF1<C1>>,
63 pub(super) i_usize: Option<usize>,
64 pub(super) z_0: Option<Vec<C1::ScalarField>>,
65 pub(super) z_i: Option<Vec<C1::ScalarField>>,
66 pub(super) external_inputs: Option<Vec<C1::ScalarField>>,
67 pub(super) u_i_cmW: Option<C1>,
68 pub(super) U_i: Option<CommittedInstance<C1>>,
69 pub(super) U_i1_cmE: Option<C1>,
70 pub(super) U_i1_cmW: Option<C1>,
71 pub(super) cmT: Option<C1>,
72 pub(super) F: FC, // F circuit
73 pub(super) x: Option<CF1<C1>>, // public input (u_{i+1}.x[0])
74
75 // cyclefold verifier on C1
76 // Here 'cf1, cf2' are for each of the CycleFold circuits, corresponding to the fold of cmW and
77 // cmE respectively
78 pub(super) cf1_u_i_cmW: Option<C2>, // input
79 pub(super) cf2_u_i_cmW: Option<C2>, // input
80 pub(super) cf_U_i: Option<CycleFoldCommittedInstance<C2>>, // input
81 pub(super) cf1_cmT: Option<C2>,
82 pub(super) cf2_cmT: Option<C2>,
83 pub(super) cf_x: Option<CF1<C1>>, // public input (u_{i+1}.x[1])
84}
85
86impl<C1: CurveGroup, C2: CurveGroup, GC2: CurveVar<C2, CF2<C2>>, FC: FCircuit<CF1<C1>>>
87 AugmentedFCircuit<C1, C2, GC2, FC>
88{
89 pub fn empty(poseidon_config: &PoseidonConfig<CF1<C1>>, F_circuit: FC) -> Self {
90 Self {
91 _gc2: PhantomData,
92 poseidon_config: poseidon_config.clone(),
93 pp_hash: None,
94 i: None,
95 i_usize: None,
96 z_0: None,
97 z_i: None,
98 external_inputs: None,
99 u_i_cmW: None,
100 U_i: None,
101 U_i1_cmE: None,
102 U_i1_cmW: None,
103 cmT: None,
104 F: F_circuit,
105 x: None,
106 // cyclefold values
107 cf1_u_i_cmW: None,
108 cf2_u_i_cmW: None,
109 cf_U_i: None,
110 cf1_cmT: None,
111 cf2_cmT: None,
112 cf_x: None,
113 }
114 }
115}
116
117impl<C1, C2, GC2, FC> ConstraintSynthesizer<CF1<C1>> for AugmentedFCircuit<C1, C2, GC2, FC>
118where
119 C1: CurveGroup,
120 C2: CurveGroup,
121 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
122 FC: FCircuit<CF1<C1>>,
123 <C1 as CurveGroup>::BaseField: PrimeField,
124 <C2 as CurveGroup>::BaseField: PrimeField,
125 <C1 as Group>::ScalarField: Absorb,
126 <C2 as Group>::ScalarField: Absorb,
127 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
128{
129 fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C1>>) -> Result<(), SynthesisError> {
130 let pp_hash = FpVar::<CF1<C1>>::new_witness(cs.clone(), || {
131 Ok(self.pp_hash.unwrap_or_else(CF1::<C1>::zero))
132 })?;
133 let i = FpVar::<CF1<C1>>::new_witness(cs.clone(), || {
134 Ok(self.i.unwrap_or_else(CF1::<C1>::zero))
135 })?;
136 let z_0 = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
137 Ok(self
138 .z_0
139 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
140 })?;
141 let z_i = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
142 Ok(self
143 .z_i
144 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
145 })?;
146 let external_inputs = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
147 Ok(self
148 .external_inputs
149 .unwrap_or(vec![CF1::<C1>::zero(); self.F.external_inputs_len()]))
150 })?;
151
152 let u_dummy = CommittedInstance::dummy(2);
153 let U_i = CommittedInstanceVar::<C1>::new_witness(cs.clone(), || {
154 Ok(self.U_i.unwrap_or(u_dummy.clone()))
155 })?;
156 let U_i1_cmE = NonNativeAffineVar::new_witness(cs.clone(), || {
157 Ok(self.U_i1_cmE.unwrap_or_else(C1::zero))
158 })?;
159 let U_i1_cmW = NonNativeAffineVar::new_witness(cs.clone(), || {
160 Ok(self.U_i1_cmW.unwrap_or_else(C1::zero))
161 })?;
162
163 let cmT =
164 NonNativeAffineVar::new_witness(cs.clone(), || Ok(self.cmT.unwrap_or_else(C1::zero)))?;
165
166 let cf_u_dummy = CycleFoldCommittedInstance::dummy(NovaCycleFoldConfig::<C1>::IO_LEN);
167 let cf_U_i = CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || {
168 Ok(self.cf_U_i.unwrap_or(cf_u_dummy.clone()))
169 })?;
170 let cf1_cmT = GC2::new_witness(cs.clone(), || Ok(self.cf1_cmT.unwrap_or_else(C2::zero)))?;
171 let cf2_cmT = GC2::new_witness(cs.clone(), || Ok(self.cf2_cmT.unwrap_or_else(C2::zero)))?;
172
173 // `sponge` is for digest computation.
174 let sponge = PoseidonSpongeVar::<C1::ScalarField>::new(cs.clone(), &self.poseidon_config);
175 // `transcript` is for challenge generation.
176 let mut transcript = sponge.clone();
177
178 let is_basecase = i.is_zero()?;
179
180 // Primary Part
181 // P.1. Compute u_i.x
182 // u_i.x[0] = H(i, z_0, z_i, U_i)
183 let (u_i_x, U_i_vec) = U_i.clone().hash(&sponge, &pp_hash, &i, &z_0, &z_i)?;
184 // u_i.x[1] = H(cf_U_i)
185 let (cf_u_i_x, cf_U_i_vec) = cf_U_i.clone().hash(&sponge, pp_hash.clone())?;
186
187 // P.2. Construct u_i
188 let u_i = CommittedInstanceVar {
189 // u_i.cmE = cm(0)
190 cmE: NonNativeAffineVar::new_constant(cs.clone(), C1::zero())?,
191 // u_i.u = 1
192 u: FpVar::one(),
193 // u_i.cmW is provided by the prover as witness
194 cmW: NonNativeAffineVar::new_witness(cs.clone(), || {
195 Ok(self.u_i_cmW.unwrap_or(C1::zero()))
196 })?,
197 // u_i.x is computed in step 1
198 x: vec![u_i_x, cf_u_i_x],
199 };
200
201 // P.3. nifs.verify, obtains U_{i+1} by folding u_i & U_i.
202 // Notice that NIFSGadget::verify does not fold cmE & cmW.
203 // We set `U_i1.cmE` and `U_i1.cmW` to unconstrained witnesses `U_i1_cmE` and `U_i1_cmW`
204 // respectively.
205 // The correctness of them will be checked on the other curve.
206 let (mut U_i1, r_bits) = NIFSGadget::<
207 C1,
208 PoseidonSponge<C1::ScalarField>,
209 PoseidonSpongeVar<C1::ScalarField>,
210 >::verify(
211 &mut transcript,
212 pp_hash.clone(),
213 U_i.clone(),
214 U_i_vec,
215 u_i.clone(),
216 Some(cmT.clone()),
217 )?;
218 U_i1.cmE = U_i1_cmE;
219 U_i1.cmW = U_i1_cmW;
220
221 // convert r_bits to a `NonNativeFieldVar`
222 let r_nonnat = {
223 let mut bits = r_bits;
224 bits.resize(C1::BaseField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
225 NonNativeUintVar::from(&bits)
226 };
227
228 // P.4.a compute and check the first output of F'
229
230 // get z_{i+1} from the F circuit
231 let i_usize = self.i_usize.unwrap_or(0);
232 let z_i1 = self
233 .F
234 .generate_step_constraints(cs.clone(), i_usize, z_i, external_inputs)?;
235
236 // Base case: u_{i+1}.x[0] == H((i+1, z_0, z_{i+1}, U_{\bot})
237 // Non-base case: u_{i+1}.x[0] == H((i+1, z_0, z_{i+1}, U_{i+1})
238 let (u_i1_x, _) = U_i1.clone().hash(
239 &sponge,
240 &pp_hash,
241 &(i + FpVar::<CF1<C1>>::one()),
242 &z_0,
243 &z_i1,
244 )?;
245 let (u_i1_x_base, _) = CommittedInstanceVar::new_constant(cs.clone(), u_dummy)?.hash(
246 &sponge,
247 &pp_hash,
248 &FpVar::<CF1<C1>>::one(),
249 &z_0,
250 &z_i1,
251 )?;
252 let x = FpVar::new_input(cs.clone(), || Ok(self.x.unwrap_or(u_i1_x_base.value()?)))?;
253 x.enforce_equal(&is_basecase.select(&u_i1_x_base, &u_i1_x)?)?;
254
255 // CycleFold part
256 // C.1. Compute cf1_u_i.x and cf2_u_i.x
257 let cfW_x = vec![
258 r_nonnat.clone(),
259 U_i.cmW.x,
260 U_i.cmW.y,
261 u_i.cmW.x,
262 u_i.cmW.y,
263 U_i1.cmW.x,
264 U_i1.cmW.y,
265 ];
266 let cfE_x = vec![
267 r_nonnat, U_i.cmE.x, U_i.cmE.y, cmT.x, cmT.y, U_i1.cmE.x, U_i1.cmE.y,
268 ];
269
270 // ensure that cf1_u & cf2_u have as public inputs the cmW & cmE from main instances U_i,
271 // u_i, U_i+1 coordinates of the commitments
272 // C.2. Construct `cf1_u_i` and `cf2_u_i`
273 let cf1_u_i = CycleFoldCommittedInstanceVar {
274 // cf1_u_i.cmE = 0
275 cmE: GC2::zero(),
276 // cf1_u_i.u = 1
277 u: NonNativeUintVar::new_constant(cs.clone(), C1::BaseField::one())?,
278 // cf1_u_i.cmW is provided by the prover as witness
279 cmW: GC2::new_witness(cs.clone(), || Ok(self.cf1_u_i_cmW.unwrap_or(C2::zero())))?,
280 // cf1_u_i.x is computed in step 1
281 x: cfW_x,
282 };
283 let cf2_u_i = CycleFoldCommittedInstanceVar {
284 // cf2_u_i.cmE = 0
285 cmE: GC2::zero(),
286 // cf2_u_i.u = 1
287 u: NonNativeUintVar::new_constant(cs.clone(), C1::BaseField::one())?,
288 // cf2_u_i.cmW is provided by the prover as witness
289 cmW: GC2::new_witness(cs.clone(), || Ok(self.cf2_u_i_cmW.unwrap_or(C2::zero())))?,
290 // cf2_u_i.x is computed in step 1
291 x: cfE_x,
292 };
293
294 // C.3. nifs.verify, obtains cf1_U_{i+1} by folding cf1_u_i & cf_U_i, and then cf_U_{i+1}
295 // by folding cf2_u_i & cf1_U_{i+1}.
296
297 // compute cf1_r = H(cf1_u_i, cf_U_i, cf1_cmT)
298 // cf_r_bits is denoted by rho* in the paper.
299 let cf1_r_bits = CycleFoldChallengeGadget::<C2, GC2>::get_challenge_gadget(
300 &mut transcript,
301 pp_hash.clone(),
302 cf_U_i_vec,
303 cf1_u_i.clone(),
304 cf1_cmT.clone(),
305 )?;
306 // Fold cf1_u_i & cf_U_i into cf1_U_{i+1}
307 let cf1_U_i1 = NIFSFullGadget::<C2, GC2>::fold_committed_instance(
308 cf1_r_bits, cf1_cmT, cf_U_i, cf1_u_i,
309 )?;
310
311 // same for cf2_r:
312 let cf2_r_bits = CycleFoldChallengeGadget::<C2, GC2>::get_challenge_gadget(
313 &mut transcript,
314 pp_hash.clone(),
315 cf1_U_i1.to_native_sponge_field_elements()?,
316 cf2_u_i.clone(),
317 cf2_cmT.clone(),
318 )?;
319 let cf_U_i1 = NIFSFullGadget::<C2, GC2>::fold_committed_instance(
320 cf2_r_bits, cf2_cmT, cf1_U_i1, // the output from NIFS.V(cf1_r, cf_U, cfE_u)
321 cf2_u_i,
322 )?;
323
324 // Back to Primary Part
325 // P.4.b compute and check the second output of F'
326 // Base case: u_{i+1}.x[1] == H(cf_U_{\bot})
327 // Non-base case: u_{i+1}.x[1] == H(cf_U_{i+1})
328 let (cf_u_i1_x, _) = cf_U_i1.clone().hash(&sponge, pp_hash.clone())?;
329 let (cf_u_i1_x_base, _) =
330 CycleFoldCommittedInstanceVar::<C2, GC2>::new_constant(cs.clone(), cf_u_dummy)?
331 .hash(&sponge, pp_hash)?;
332 let cf_x = FpVar::new_input(cs.clone(), || {
333 Ok(self.cf_x.unwrap_or(cf_u_i1_x_base.value()?))
334 })?;
335 cf_x.enforce_equal(&is_basecase.select(&cf_u_i1_x_base, &cf_u_i1_x)?)?;
336
337 Ok(())
338 }
339}
340
341#[cfg(test)]
342pub mod tests {
343 use super::*;
344 use ark_bn254::{Fr, G1Projective as Projective};
345 use ark_crypto_primitives::sponge::{poseidon::PoseidonSponge, CryptographicSponge};
346 use ark_ff::BigInteger;
347 use ark_relations::r1cs::ConstraintSystem;
348 use ark_std::UniformRand;
349
350 use crate::folding::nova::nifs::nova::ChallengeGadget;
351 use crate::transcript::poseidon::poseidon_canonical_config;
352
353 // checks that the gadget and native implementations of the challenge computation match
354 #[test]
355 fn test_challenge_gadget() {
356 let mut rng = ark_std::test_rng();
357 let poseidon_config = poseidon_canonical_config::<Fr>();
358 let mut transcript = PoseidonSponge::<Fr>::new(&poseidon_config);
359
360 let u_i = CommittedInstance::<Projective> {
361 cmE: Projective::rand(&mut rng),
362 u: Fr::rand(&mut rng),
363 cmW: Projective::rand(&mut rng),
364 x: vec![Fr::rand(&mut rng); 1],
365 };
366 let U_i = CommittedInstance::<Projective> {
367 cmE: Projective::rand(&mut rng),
368 u: Fr::rand(&mut rng),
369 cmW: Projective::rand(&mut rng),
370 x: vec![Fr::rand(&mut rng); 1],
371 };
372 let cmT = Projective::rand(&mut rng);
373
374 let pp_hash = Fr::from(42u32); // only for testing
375
376 // compute the challenge natively
377 let r_bits =
378 ChallengeGadget::<Projective, CommittedInstance<Projective>>::get_challenge_native(
379 &mut transcript,
380 pp_hash,
381 &U_i,
382 &u_i,
383 Some(&cmT),
384 );
385 let r = Fr::from_bigint(BigInteger::from_bits_le(&r_bits)).unwrap();
386
387 let cs = ConstraintSystem::<Fr>::new_ref();
388 let pp_hashVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(pp_hash)).unwrap();
389 let u_iVar =
390 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(u_i.clone()))
391 .unwrap();
392 let U_iVar =
393 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(U_i.clone()))
394 .unwrap();
395 let cmTVar = NonNativeAffineVar::<Projective>::new_witness(cs.clone(), || Ok(cmT)).unwrap();
396 let mut transcriptVar = PoseidonSpongeVar::<Fr>::new(cs.clone(), &poseidon_config);
397
398 // compute the challenge in-circuit
399 let U_iVar_vec = [
400 vec![U_iVar.u.clone()],
401 U_iVar.x.clone(),
402 U_iVar.cmE.to_constraint_field().unwrap(),
403 U_iVar.cmW.to_constraint_field().unwrap(),
404 ]
405 .concat();
406 let r_bitsVar =
407 ChallengeGadget::<Projective, CommittedInstance<Projective>>::get_challenge_gadget(
408 &mut transcriptVar,
409 pp_hashVar,
410 U_iVar_vec,
411 u_iVar,
412 Some(cmTVar),
413 )
414 .unwrap();
415 assert!(cs.is_satisfied().unwrap());
416
417 // check that the natively computed and in-circuit computed hashes match
418 let rVar = Boolean::le_bits_to_fp_var(&r_bitsVar).unwrap();
419 assert_eq!(rVar.value().unwrap(), r);
420 assert_eq!(r_bitsVar.value().unwrap(), r_bits);
421 }
422}