sonobe/src/folding/nova/circuits.rs
src/folding/nova/circuits.rsRaw
1use ark_crypto_primitives::crh::{
2 poseidon::constraints::{CRHGadget, CRHParametersVar},
3 CRHSchemeGadget,
4};
5use ark_crypto_primitives::sponge::Absorb;
6use ark_ec::{AffineRepr, CurveGroup, Group};
7use ark_ff::Field;
8use ark_r1cs_std::{
9 alloc::{AllocVar, AllocationMode},
10 boolean::Boolean,
11 eq::EqGadget,
12 fields::fp::FpVar,
13 groups::GroupOpsBounds,
14 prelude::CurveVar,
15 ToConstraintFieldGadget,
16};
17use ark_relations::r1cs::{Namespace, SynthesisError};
18use core::{borrow::Borrow, marker::PhantomData};
19
20use super::CommittedInstance;
21use crate::folding::circuits::{cyclefold::ECRLC, nonnative::NonNativeAffineVar};
22
23/// CF1 represents the ConstraintField used for the main Nova circuit which is over E1::Fr, where
24/// E1 is the main curve where we do the folding.
25pub type CF1<C> = <<C as CurveGroup>::Affine as AffineRepr>::ScalarField;
26/// CF2 represents the ConstraintField used for the CycleFold circuit which is over E2::Fr=E1::Fq,
27/// where E2 is the auxiliary curve (from [CycleFold](https://eprint.iacr.org/2023/1192.pdf)
28/// approach) where we check the folding of the commitments.
29pub type CF2<C> = <<C as CurveGroup>::BaseField as Field>::BasePrimeField;
30
31/// CommittedInstanceVar contains the u, x, cmE and cmW values which are folded on the main Nova
32/// constraints field (E1::Fr, where E1 is the main curve).
33#[derive(Debug, Clone)]
34pub struct CommittedInstanceVar<C: CurveGroup> {
35 _c: PhantomData<C>,
36 u: FpVar<C::ScalarField>,
37 x: Vec<FpVar<C::ScalarField>>,
38 #[allow(dead_code)] // tmp while we don't have the code of the AugmentedFGadget
39 cmE: NonNativeAffineVar<CF2<C>, C::ScalarField>,
40 cmW: NonNativeAffineVar<CF2<C>, C::ScalarField>,
41}
42
43impl<C> AllocVar<CommittedInstance<C>, CF1<C>> for CommittedInstanceVar<C>
44where
45 C: CurveGroup,
46 <C as ark_ec::CurveGroup>::BaseField: ark_ff::PrimeField,
47{
48 fn new_variable<T: Borrow<CommittedInstance<C>>>(
49 cs: impl Into<Namespace<CF1<C>>>,
50 f: impl FnOnce() -> Result<T, SynthesisError>,
51 mode: AllocationMode,
52 ) -> Result<Self, SynthesisError> {
53 f().and_then(|val| {
54 let cs = cs.into();
55
56 let u = FpVar::<C::ScalarField>::new_variable(cs.clone(), || Ok(val.borrow().u), mode)?;
57 let x: Vec<FpVar<C::ScalarField>> =
58 Vec::new_variable(cs.clone(), || Ok(val.borrow().x.clone()), mode)?;
59
60 let cmE = NonNativeAffineVar::<CF2<C>, C::ScalarField>::new_variable(
61 cs.clone(),
62 || Ok(val.borrow().cmE),
63 mode,
64 )?;
65 let cmW = NonNativeAffineVar::<CF2<C>, C::ScalarField>::new_variable(
66 cs.clone(),
67 || Ok(val.borrow().cmW),
68 mode,
69 )?;
70
71 Ok(Self {
72 _c: PhantomData,
73 u,
74 x,
75 cmE,
76 cmW,
77 })
78 })
79 }
80}
81
82impl<C> CommittedInstanceVar<C>
83where
84 C: CurveGroup,
85 <C as Group>::ScalarField: Absorb,
86{
87 /// hash implements the committed instance hash compatible with the native implementation from
88 /// CommittedInstance.hash.
89 /// Returns `H(i, z_0, z_i, U_i)`, where `i` can be `i` but also `i+1`, and `U` is the
90 /// `CommittedInstance`.
91 #[allow(dead_code)] // tmp while we don't have the code of the AugmentedFGadget
92 fn hash(
93 self,
94 crh_params: &CRHParametersVar<CF1<C>>,
95 i: FpVar<CF1<C>>,
96 z_0: FpVar<CF1<C>>,
97 z_i: FpVar<CF1<C>>,
98 ) -> Result<FpVar<CF1<C>>, SynthesisError> {
99 let input = vec![
100 vec![i, z_0, z_i, self.u],
101 self.x,
102 self.cmE.x.to_constraint_field()?,
103 self.cmE.y.to_constraint_field()?,
104 self.cmW.x.to_constraint_field()?,
105 self.cmW.y.to_constraint_field()?,
106 ]
107 .concat();
108 CRHGadget::<C::ScalarField>::evaluate(crh_params, &input)
109 }
110}
111
112/// CommittedInstanceCycleFoldVar represents the commitments to E and W from the CommittedInstance
113/// on the E2, which are folded on the auxiliary curve constraints field (E2::Fr = E1::Fq).
114pub struct CommittedInstanceCycleFoldVar<C: CurveGroup, GC: CurveVar<C, CF2<C>>>
115where
116 for<'a> &'a GC: GroupOpsBounds<'a, C, GC>,
117{
118 _c: PhantomData<C>,
119 cmE: GC,
120 cmW: GC,
121}
122
123impl<C, GC> AllocVar<CommittedInstance<C>, CF2<C>> for CommittedInstanceCycleFoldVar<C, GC>
124where
125 C: CurveGroup,
126 GC: CurveVar<C, CF2<C>>,
127 for<'a> &'a GC: GroupOpsBounds<'a, C, GC>,
128{
129 fn new_variable<T: Borrow<CommittedInstance<C>>>(
130 cs: impl Into<Namespace<CF2<C>>>,
131 f: impl FnOnce() -> Result<T, SynthesisError>,
132 mode: AllocationMode,
133 ) -> Result<Self, SynthesisError> {
134 f().and_then(|val| {
135 let cs = cs.into();
136
137 let cmE = GC::new_variable(cs.clone(), || Ok(val.borrow().cmE), mode)?;
138 let cmW = GC::new_variable(cs.clone(), || Ok(val.borrow().cmW), mode)?;
139
140 Ok(Self {
141 _c: PhantomData,
142 cmE,
143 cmW,
144 })
145 })
146 }
147}
148
149/// Implements the circuit that does the checks of the Non-Interactive Folding Scheme Verifier
150/// described in section 4 of [Nova](https://eprint.iacr.org/2021/370.pdf), where the cmE & cmW checks are
151/// delegated to the NIFSCycleFoldGadget.
152pub struct NIFSGadget<C: CurveGroup> {
153 _c: PhantomData<C>,
154}
155
156impl<C: CurveGroup> NIFSGadget<C>
157where
158 C: CurveGroup,
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>,
165 ci2: CommittedInstanceVar<C>,
166 ci3: CommittedInstanceVar<C>,
167 ) -> Result<(), SynthesisError> {
168 // ensure that: ci3.u == ci1.u + r * ci2.u
169 ci3.u.enforce_equal(&(ci1.u + r.clone() * ci2.u))?;
170
171 // ensure that: ci3.x == ci1.x + r * ci2.x
172 let x_rlc = ci1
173 .x
174 .iter()
175 .zip(ci2.x)
176 .map(|(a, b)| a + &r * &b)
177 .collect::<Vec<FpVar<CF1<C>>>>();
178 x_rlc.enforce_equal(&ci3.x)?;
179
180 Ok(())
181 }
182}
183
184/// NIFSCycleFoldGadget performs the Nova NIFS.V elliptic curve points relation checks in the other
185/// curve following [CycleFold](https://eprint.iacr.org/2023/1192.pdf).
186pub struct NIFSCycleFoldGadget<C: CurveGroup, GC: CurveVar<C, CF2<C>>> {
187 _c: PhantomData<C>,
188 _gc: PhantomData<GC>,
189}
190impl<C: CurveGroup, GC: CurveVar<C, CF2<C>>> NIFSCycleFoldGadget<C, GC>
191where
192 C: CurveGroup,
193 GC: CurveVar<C, CF2<C>>,
194 for<'a> &'a GC: GroupOpsBounds<'a, C, GC>,
195{
196 pub fn verify(
197 r_bits: Vec<Boolean<CF2<C>>>,
198 cmT: GC,
199 ci1: CommittedInstanceCycleFoldVar<C, GC>,
200 ci2: CommittedInstanceCycleFoldVar<C, GC>,
201 ci3: CommittedInstanceCycleFoldVar<C, GC>,
202 ) -> Result<(), SynthesisError> {
203 // cm(E) check: ci3.cmE == ci1.cmE + r * cmT + r^2 * ci2.cmE
204 ci3.cmE.enforce_equal(
205 &((ci2.cmE.scalar_mul_le(r_bits.iter())? + cmT).scalar_mul_le(r_bits.iter())?
206 + ci1.cmE),
207 )?;
208 // cm(W) check: ci3.cmW == ci1.cmW + r * ci2.cmW
209 ECRLC::<C, GC>::check(r_bits, ci1.cmW, ci2.cmW, ci3.cmW)?;
210 Ok(())
211 }
212}
213
214#[cfg(test)]
215mod tests {
216 use super::*;
217 use ark_ff::{BigInteger, PrimeField};
218 use ark_pallas::{constraints::GVar, Fq, Fr, Projective};
219 use ark_r1cs_std::{alloc::AllocVar, R1CSVar};
220 use ark_relations::r1cs::ConstraintSystem;
221 use ark_std::UniformRand;
222
223 use crate::ccs::r1cs::tests::{get_test_r1cs, get_test_z};
224 use crate::folding::nova::{nifs::NIFS, Witness};
225 use crate::pedersen::Pedersen;
226 use crate::transcript::poseidon::{tests::poseidon_test_config, PoseidonTranscript};
227 use crate::transcript::Transcript;
228
229 #[test]
230 fn test_committed_instance_var() {
231 let mut rng = ark_std::test_rng();
232
233 let ci = CommittedInstance::<Projective> {
234 cmE: Projective::rand(&mut rng),
235 u: Fr::rand(&mut rng),
236 cmW: Projective::rand(&mut rng),
237 x: vec![Fr::rand(&mut rng); 1],
238 };
239
240 let cs = ConstraintSystem::<Fr>::new_ref();
241 let ciVar =
242 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci.clone())).unwrap();
243 assert_eq!(ciVar.u.value().unwrap(), ci.u);
244 assert_eq!(ciVar.x.value().unwrap(), ci.x);
245
246 // check the instantiation of the CycleFold side:
247 let cs = ConstraintSystem::<Fq>::new_ref();
248 let ciVar =
249 CommittedInstanceCycleFoldVar::<Projective, GVar>::new_witness(cs.clone(), || {
250 Ok(ci.clone())
251 })
252 .unwrap();
253 assert_eq!(ciVar.cmE.value().unwrap(), ci.cmE);
254 assert_eq!(ciVar.cmW.value().unwrap(), ci.cmW);
255 }
256
257 #[test]
258 fn test_nifs_gadget() {
259 let r1cs = get_test_r1cs();
260 let z1 = get_test_z(3);
261 let z2 = get_test_z(4);
262 let (w1, x1) = r1cs.split_z(&z1);
263 let (w2, x2) = r1cs.split_z(&z2);
264
265 let w1 = Witness::<Projective>::new(w1.clone(), r1cs.A.n_rows);
266 let w2 = Witness::<Projective>::new(w2.clone(), r1cs.A.n_rows);
267
268 let mut rng = ark_std::test_rng();
269 let pedersen_params = Pedersen::<Projective>::new_params(&mut rng, r1cs.A.n_cols);
270
271 // compute committed instances
272 let ci1 = w1.commit(&pedersen_params, x1.clone());
273 let ci2 = w2.commit(&pedersen_params, x2.clone());
274
275 // get challenge from transcript
276 let poseidon_config = poseidon_test_config::<Fr>();
277 let mut tr = PoseidonTranscript::<Projective>::new(&poseidon_config);
278 let r_bits = tr.get_challenge_nbits(128);
279 let r_Fr = Fr::from_bigint(BigInteger::from_bits_le(&r_bits)).unwrap();
280
281 let (_w3, ci3, _T, cmT) =
282 NIFS::<Projective>::prove(&pedersen_params, r_Fr, &r1cs, &w1, &ci1, &w2, &ci2).unwrap();
283
284 let cs = ConstraintSystem::<Fr>::new_ref();
285
286 let rVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(r_Fr)).unwrap();
287 let ci1Var =
288 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci1.clone()))
289 .unwrap();
290 let ci2Var =
291 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci2.clone()))
292 .unwrap();
293 let ci3Var =
294 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci3.clone()))
295 .unwrap();
296
297 NIFSGadget::<Projective>::verify(
298 rVar.clone(),
299 ci1Var.clone(),
300 ci2Var.clone(),
301 ci3Var.clone(),
302 )
303 .unwrap();
304 assert!(cs.is_satisfied().unwrap());
305
306 // cs_CC is the Constraint System on the Curve Cycle auxiliary curve constraints field
307 // (E2::Fr)
308 let cs_CC = ConstraintSystem::<Fq>::new_ref();
309
310 let r_bitsVar = Vec::<Boolean<Fq>>::new_witness(cs_CC.clone(), || Ok(r_bits)).unwrap();
311
312 let cmTVar = GVar::new_witness(cs_CC.clone(), || Ok(cmT)).unwrap();
313 let ci1Var =
314 CommittedInstanceCycleFoldVar::<Projective, GVar>::new_witness(cs_CC.clone(), || {
315 Ok(ci1.clone())
316 })
317 .unwrap();
318 let ci2Var =
319 CommittedInstanceCycleFoldVar::<Projective, GVar>::new_witness(cs_CC.clone(), || {
320 Ok(ci2.clone())
321 })
322 .unwrap();
323 let ci3Var =
324 CommittedInstanceCycleFoldVar::<Projective, GVar>::new_witness(cs_CC.clone(), || {
325 Ok(ci3.clone())
326 })
327 .unwrap();
328
329 NIFSCycleFoldGadget::<Projective, GVar>::verify(r_bitsVar, cmTVar, ci1Var, ci2Var, ci3Var)
330 .unwrap();
331 assert!(cs_CC.is_satisfied().unwrap());
332 }
333
334 #[test]
335 fn test_committed_instance_hash() {
336 let mut rng = ark_std::test_rng();
337 let poseidon_config = poseidon_test_config::<Fr>();
338
339 let i = Fr::from(3_u32);
340 let z_0 = Fr::from(3_u32);
341 let z_i = Fr::from(3_u32);
342 let ci = CommittedInstance::<Projective> {
343 cmE: Projective::rand(&mut rng),
344 u: Fr::rand(&mut rng),
345 cmW: Projective::rand(&mut rng),
346 x: vec![Fr::rand(&mut rng); 1],
347 };
348
349 // compute the CommittedInstance hash natively
350 let h = ci.hash(&poseidon_config, i, z_0, z_i).unwrap();
351
352 let cs = ConstraintSystem::<Fr>::new_ref();
353
354 let iVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(i)).unwrap();
355 let z_0Var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(z_0)).unwrap();
356 let z_iVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(z_i)).unwrap();
357 let ciVar =
358 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci.clone())).unwrap();
359
360 let crh_params = CRHParametersVar::<Fr>::new_constant(cs.clone(), poseidon_config).unwrap();
361
362 // compute the CommittedInstance hash in-circuit
363 let hVar = ciVar.hash(&crh_params, iVar, z_0Var, z_iVar).unwrap();
364 assert!(cs.is_satisfied().unwrap());
365
366 // check that the natively computed and in-circuit computed hashes match
367 assert_eq!(hVar.value().unwrap(), h);
368 }
369}