sonobe/folding-schemes/src/folding/circuits/decider/on_chain.rs
folding-schemes/src/folding/circuits/decider/on_chain.rsRaw
1/// This file implements the onchain (Ethereum's EVM) decider circuit. For non-ethereum use cases,
2/// other more efficient approaches can be used.
3use ark_crypto_primitives::sponge::{
4 constraints::{AbsorbGadget, CryptographicSpongeVar},
5 poseidon::{constraints::PoseidonSpongeVar, PoseidonConfig},
6 Absorb,
7};
8use ark_ec::CurveGroup;
9use ark_r1cs_std::{
10 alloc::AllocVar, eq::EqGadget, fields::fp::FpVar, prelude::CurveVar, ToConstraintFieldGadget,
11};
12use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystemRef, SynthesisError};
13use ark_std::{marker::PhantomData, Zero};
14
15use crate::{
16 arith::{r1cs::R1CS, Arith, ArithGadget},
17 commitment::pedersen::Params as PedersenParams,
18 folding::{
19 circuits::{
20 cyclefold::{
21 CycleFoldCommittedInstance, CycleFoldCommittedInstanceVar, CycleFoldWitness,
22 },
23 decider::{EvalGadget, KZGChallengesGadget},
24 nonnative::affine::NonNativeAffineVar,
25 CF1, CF2,
26 },
27 traits::{CommittedInstanceOps, CommittedInstanceVarOps, Dummy, WitnessOps, WitnessVarOps},
28 },
29};
30
31use super::DeciderEnabledNIFS;
32
33/// A generic circuit tailored for the onchain (Ethereum's EVM) verification of
34/// IVC proofs, where we support IVC built upon any folding scheme.
35///
36/// Specifically, `GenericDeciderEthCircuit` implements the in-circuit version
37/// of the IVC verification algorithm, which essentially checks the following:
38/// - `R_arith(W_i, U_i)`:
39/// The running instance `U_i` and witness `W_i` satisfy `arith`,
40/// and the commitments in `U_i` open to the values in `W_i`.
41/// - `R_arith(w_i, u_i)`:
42/// The incoming instance `u_i` and witness `w_i` satisfy `arith`,
43/// and the commitments in `u_i` open to the values in `w_i`.
44/// - `R_cf_arith(cf_W_i, cf_U_i)`:
45/// The CycleFold instance `cf_U_i` and witness `cf_W_i` satisfy `cf_arith`,
46/// and the commitments in `cf_U_i` open to the values in `cf_W_i`.
47/// - `u_i` contains the correct hash of the initial and final states.
48///
49/// To reduce the number of relation checks, the prover, before invoking the
50/// circuit, further folds `U_i, u_i` into `U_{i+1}`, and `W_i, w_i` into
51/// `W_{i+1}`.
52/// Now, the circuit only needs to perform two relation checks, i.e.,
53/// `R_arith(W_{i+1}, U_{i+1})` and `R_cf_arith(cf_W_i, cf_U_i)`, plus a few
54/// constraints for enforcing the correct hash in `u_i` and the correct folding
55/// from `U_i, u_i` to `U_{i+1}`.
56///
57/// We further reduce the circuit size by avoiding the non-native commitment
58/// checks involved in `R_arith(W_{i+1}, U_{i+1})`.
59/// Now, we now only check the satisfiability of the constraint system `arith`
60/// with the witness `W_{i+1}` and instance `U_{i+1}` in the circuit, but the
61/// actual commitment checks are done with the help of KZG.
62///
63/// For more details, see [https://privacy-scaling-explorations.github.io/sonobe-docs/design/nova-decider-onchain.html].
64pub struct GenericOnchainDeciderCircuit<
65 C1: CurveGroup,
66 C2: CurveGroup,
67 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
68 RU: CommittedInstanceOps<C1>, // Running instance
69 IU: CommittedInstanceOps<C1>, // Incoming instance
70 W: WitnessOps<CF1<C1>>, // Witness
71 A: Arith<W, RU>, // Constraint system
72 AVar: ArithGadget<W::Var, RU::Var>, // In-circuit representation of `A`
73 D: DeciderEnabledNIFS<C1, RU, IU, W, A>,
74> {
75 pub _gc2: PhantomData<GC2>,
76 pub _avar: PhantomData<AVar>,
77 /// Constraint system of the Augmented Function circuit
78 pub arith: A,
79 /// R1CS of the CycleFold circuit
80 pub cf_arith: R1CS<CF1<C2>>,
81 /// CycleFold PedersenParams over C2
82 pub cf_pedersen_params: PedersenParams<C2>,
83 pub poseidon_config: PoseidonConfig<CF1<C1>>,
84 /// public params hash
85 pub pp_hash: CF1<C1>,
86 pub i: CF1<C1>,
87 /// initial state
88 pub z_0: Vec<CF1<C1>>,
89 /// current i-th state
90 pub z_i: Vec<CF1<C1>>,
91 /// Folding scheme instances
92 pub U_i: RU,
93 pub W_i: W,
94 pub u_i: IU,
95 pub w_i: W,
96 pub U_i1: RU,
97 pub W_i1: W,
98
99 /// Helper for folding verification
100 pub proof: D::Proof,
101 pub randomness: D::Randomness,
102
103 /// CycleFold running instance
104 pub cf_U_i: CycleFoldCommittedInstance<C2>,
105 pub cf_W_i: CycleFoldWitness<C2>,
106
107 /// KZG challenges
108 pub kzg_challenges: Vec<CF1<C1>>,
109 pub kzg_evaluations: Vec<CF1<C1>>,
110}
111
112impl<
113 C1: CurveGroup,
114 C2: CurveGroup<ScalarField = CF2<C1>, BaseField = CF1<C1>>,
115 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
116 RU: CommittedInstanceOps<C1> + for<'a> Dummy<&'a A>,
117 IU: CommittedInstanceOps<C1> + for<'a> Dummy<&'a A>,
118 W: WitnessOps<CF1<C1>> + for<'a> Dummy<&'a A>,
119 A: Arith<W, RU>,
120 AVar: ArithGadget<W::Var, RU::Var> + AllocVar<A, CF1<C1>>,
121 D: DeciderEnabledNIFS<C1, RU, IU, W, A>,
122 >
123 Dummy<(
124 A,
125 R1CS<CF1<C2>>,
126 PedersenParams<C2>,
127 PoseidonConfig<CF1<C1>>,
128 D::ProofDummyCfg,
129 D::RandomnessDummyCfg,
130 usize,
131 usize,
132 )> for GenericOnchainDeciderCircuit<C1, C2, GC2, RU, IU, W, A, AVar, D>
133{
134 fn dummy(
135 (
136 arith,
137 cf_arith,
138 cf_pedersen_params,
139 poseidon_config,
140 proof_config,
141 randomness_config,
142 state_len,
143 num_commitments,
144 ): (
145 A,
146 R1CS<CF1<C2>>,
147 PedersenParams<C2>,
148 PoseidonConfig<CF1<C1>>,
149 D::ProofDummyCfg,
150 D::RandomnessDummyCfg,
151 usize,
152 usize,
153 ),
154 ) -> Self {
155 Self {
156 _gc2: PhantomData,
157 _avar: PhantomData,
158 cf_pedersen_params,
159 poseidon_config,
160 pp_hash: Zero::zero(),
161 i: Zero::zero(),
162 z_0: vec![Zero::zero(); state_len],
163 z_i: vec![Zero::zero(); state_len],
164 U_i: RU::dummy(&arith),
165 W_i: W::dummy(&arith),
166 u_i: IU::dummy(&arith),
167 w_i: W::dummy(&arith),
168 U_i1: RU::dummy(&arith),
169 W_i1: W::dummy(&arith),
170 proof: D::Proof::dummy(proof_config),
171 randomness: D::Randomness::dummy(randomness_config),
172 cf_U_i: CycleFoldCommittedInstance::dummy(&cf_arith),
173 cf_W_i: CycleFoldWitness::dummy(&cf_arith),
174 kzg_challenges: vec![Zero::zero(); num_commitments],
175 kzg_evaluations: vec![Zero::zero(); num_commitments],
176 arith,
177 cf_arith,
178 }
179 }
180}
181
182impl<
183 C1: CurveGroup,
184 C2: CurveGroup<ScalarField = CF2<C1>, BaseField = CF1<C1>>,
185 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
186 RU: CommittedInstanceOps<C1>,
187 IU: CommittedInstanceOps<C1>,
188 W: WitnessOps<CF1<C1>>,
189 A: Arith<W, RU>,
190 AVar: ArithGadget<W::Var, RU::Var> + AllocVar<A, CF1<C1>>,
191 D: DeciderEnabledNIFS<C1, RU, IU, W, A>,
192 > ConstraintSynthesizer<CF1<C1>>
193 for GenericOnchainDeciderCircuit<C1, C2, GC2, RU, IU, W, A, AVar, D>
194where
195 RU::Var: AbsorbGadget<CF1<C1>> + CommittedInstanceVarOps<C1, PointVar = NonNativeAffineVar<C1>>,
196 CF1<C1>: Absorb,
197{
198 fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C1>>) -> Result<(), SynthesisError> {
199 let arith = AVar::new_witness(cs.clone(), || Ok(&self.arith))?;
200
201 let pp_hash = FpVar::new_input(cs.clone(), || Ok(self.pp_hash))?;
202 let i = FpVar::new_input(cs.clone(), || Ok(self.i))?;
203 let z_0 = Vec::new_input(cs.clone(), || Ok(self.z_0))?;
204 let z_i = Vec::new_input(cs.clone(), || Ok(self.z_i))?;
205
206 let u_i = IU::Var::new_witness(cs.clone(), || Ok(self.u_i))?;
207 let U_i = RU::Var::new_witness(cs.clone(), || Ok(self.U_i))?;
208 // here (U_i1, W_i1) = NIFS.P( (U_i,W_i), (u_i,w_i))
209 let U_i1_commitments = Vec::<NonNativeAffineVar<C1>>::new_input(cs.clone(), || {
210 Ok(self.U_i1.get_commitments())
211 })?;
212 let U_i1 = RU::Var::new_witness(cs.clone(), || Ok(self.U_i1))?;
213 let W_i1 = W::Var::new_witness(cs.clone(), || Ok(self.W_i1))?;
214 U_i1.get_commitments().enforce_equal(&U_i1_commitments)?;
215
216 let cf_U_i =
217 CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || Ok(self.cf_U_i))?;
218
219 // allocate the inputs for the check 7.1 and 7.2
220 let kzg_challenges = Vec::new_input(cs.clone(), || Ok(self.kzg_challenges))?;
221 let kzg_evaluations = Vec::new_input(cs.clone(), || Ok(self.kzg_evaluations))?;
222
223 // `sponge` is for digest computation.
224 let sponge = PoseidonSpongeVar::new(cs.clone(), &self.poseidon_config);
225 // `transcript` is for challenge generation.
226 let mut transcript = sponge.clone();
227
228 // NOTE: we use the same enumeration as in
229 // https://privacy-scaling-explorations.github.io/sonobe-docs/design/nova-decider-onchain.html
230 // in order to make it easier to reason about.
231
232 // 1. enforce `U_{i+1}` and `W_{i+1}` satisfy `arith`
233 arith.enforce_relation(&W_i1, &U_i1)?;
234
235 // 2. enforce `u_i` is an incoming instance
236 u_i.enforce_incoming()?;
237
238 // 3. u_i.x[0] == H(i, z_0, z_i, U_i), u_i.x[1] == H(cf_U_i)
239 let (u_i_x, U_i_vec) = U_i.hash(&sponge, &pp_hash, &i, &z_0, &z_i)?;
240 let (cf_u_i_x, _) = cf_U_i.hash(&sponge, pp_hash.clone())?;
241 u_i.get_public_inputs().enforce_equal(&[u_i_x, cf_u_i_x])?;
242
243 #[cfg(feature = "light-test")]
244 log::warn!("[WARNING]: Running with the 'light-test' feature, skipping the big part of the DeciderEthCircuit.\n Only for testing purposes.");
245
246 // The following two checks (and their respective allocations) are disabled for normal
247 // tests since they take several millions of constraints and would take several minutes
248 // (and RAM) to run the test. It is active by default, and not active only when
249 // 'light-test' feature is used.
250 #[cfg(not(feature = "light-test"))]
251 {
252 // imports here instead of at the top of the file, so we avoid having multiple
253 // `#[cfg(not(test))]`
254 use crate::{
255 arith::r1cs::circuits::R1CSMatricesVar,
256 commitment::pedersen::PedersenGadget,
257 folding::circuits::{
258 cyclefold::CycleFoldWitnessVar, nonnative::uint::NonNativeUintVar,
259 },
260 };
261 use ark_r1cs_std::ToBitsGadget;
262 let cf_W_i = CycleFoldWitnessVar::<C2>::new_witness(cs.clone(), || Ok(self.cf_W_i))?;
263 // 4. check Pedersen commitments of cf_U_i.{cmE, cmW}
264 let H = GC2::constant(self.cf_pedersen_params.h);
265 let G = self
266 .cf_pedersen_params
267 .generators
268 .iter()
269 .map(|&g| GC2::constant(g.into()))
270 .collect::<Vec<_>>();
271 let cf_W_i_E_bits = cf_W_i
272 .E
273 .iter()
274 .map(|E_i| E_i.to_bits_le())
275 .collect::<Result<Vec<_>, _>>()?;
276 let cf_W_i_W_bits = cf_W_i
277 .W
278 .iter()
279 .map(|W_i| W_i.to_bits_le())
280 .collect::<Result<Vec<_>, _>>()?;
281 PedersenGadget::<C2, GC2>::commit(&H, &G, &cf_W_i_E_bits, &cf_W_i.rE.to_bits_le()?)?
282 .enforce_equal(&cf_U_i.cmE)?;
283 PedersenGadget::<C2, GC2>::commit(&H, &G, &cf_W_i_W_bits, &cf_W_i.rW.to_bits_le()?)?
284 .enforce_equal(&cf_U_i.cmW)?;
285
286 let cf_r1cs = R1CSMatricesVar::<CF1<C2>, NonNativeUintVar<CF2<C2>>>::new_constant(
287 ConstraintSystemRef::None,
288 self.cf_arith,
289 )?;
290
291 // 5. enforce `cf_U_i` and `cf_W_i` satisfy `cf_r1cs`
292 cf_r1cs.enforce_relation(&cf_W_i, &cf_U_i)?;
293 }
294
295 // 6.1. partially enforce `NIFS.V(U_i, u_i) = U_{i+1}`.
296 D::fold_field_elements_gadget(
297 &self.arith,
298 &mut transcript,
299 pp_hash,
300 U_i,
301 U_i_vec,
302 u_i,
303 self.proof,
304 self.randomness,
305 )?
306 .enforce_partial_equal(&U_i1)?;
307
308 // 7.1. compute and check KZG challenges
309 KZGChallengesGadget::get_challenges_gadget(&mut transcript, &U_i1)?
310 .enforce_equal(&kzg_challenges)?;
311
312 // 7.2. check the claimed evaluations
313 for (((v, _r), c), e) in W_i1
314 .get_openings()
315 .iter()
316 .zip(&kzg_challenges)
317 .zip(&kzg_evaluations)
318 {
319 // The randomness `_r` is currently not used.
320 EvalGadget::evaluate_gadget(v, c)?.enforce_equal(e)?;
321 }
322
323 Ok(())
324 }
325}