1/// This file implements the HyperNova's onchain (Ethereum's EVM) decider.
  2use ark_crypto_primitives::sponge::Absorb;
  3use ark_ec::{CurveGroup, Group};
  4use ark_ff::PrimeField;
  5use ark_r1cs_std::{groups::GroupOpsBounds, prelude::CurveVar, ToConstraintFieldGadget};
  6use ark_snark::SNARK;
  7use ark_std::rand::{CryptoRng, RngCore};
  8use ark_std::{One, Zero};
  9use core::marker::PhantomData;
 10
 11pub use super::decider_eth_circuit::DeciderEthCircuit;
 12use super::{lcccs::LCCCS, HyperNova};
 13use crate::commitment::{
 14    kzg::Proof as KZGProof, pedersen::Params as PedersenParams, CommitmentScheme,
 15};
 16use crate::folding::circuits::{nonnative::affine::NonNativeAffineVar, CF2};
 17use crate::frontend::FCircuit;
 18use crate::Error;
 19use crate::{Decider as DeciderTrait, FoldingScheme};
 20
 21#[derive(Debug, Clone, Eq, PartialEq)]
 22pub struct Proof<C1, CS1, S>
 23where
 24    C1: CurveGroup,
 25    CS1: CommitmentScheme<C1, ProverChallenge = C1::ScalarField, Challenge = C1::ScalarField>,
 26    S: SNARK<C1::ScalarField>,
 27{
 28    snark_proof: S::Proof,
 29    kzg_proof: CS1::Proof,
 30    // rho used at the last fold, U_{i+1}=NIMFS.V(rho, U_i, u_i), it is checked in-circuit
 31    rho: C1::ScalarField,
 32    U_i1: LCCCS<C1>, // U_{i+1}, which is checked in-circuit
 33    // the KZG challenge is provided by the prover, but in-circuit it is checked to match
 34    // the in-circuit computed computed one.
 35    kzg_challenge: C1::ScalarField,
 36}
 37
 38/// Onchain Decider, for ethereum use cases
 39#[derive(Clone, Debug)]
 40pub struct Decider<C1, GC1, C2, GC2, FC, CS1, CS2, S, FS, const MU: usize, const NU: usize> {
 41    _c1: PhantomData<C1>,
 42    _gc1: PhantomData<GC1>,
 43    _c2: PhantomData<C2>,
 44    _gc2: PhantomData<GC2>,
 45    _fc: PhantomData<FC>,
 46    _cs1: PhantomData<CS1>,
 47    _cs2: PhantomData<CS2>,
 48    _s: PhantomData<S>,
 49    _fs: PhantomData<FS>,
 50}
 51
 52impl<C1, GC1, C2, GC2, FC, CS1, CS2, S, FS, const MU: usize, const NU: usize>
 53    DeciderTrait<C1, C2, FC, FS> for Decider<C1, GC1, C2, GC2, FC, CS1, CS2, S, FS, MU, NU>
 54where
 55    C1: CurveGroup,
 56    C2: CurveGroup,
 57    GC1: CurveVar<C1, CF2<C1>> + ToConstraintFieldGadget<CF2<C1>>,
 58    GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
 59    FC: FCircuit<C1::ScalarField>,
 60    // CS1 is a KZG commitment, where challenge is C1::Fr elem
 61    CS1: CommitmentScheme<
 62        C1,
 63        ProverChallenge = C1::ScalarField,
 64        Challenge = C1::ScalarField,
 65        Proof = KZGProof<C1>,
 66    >,
 67    // enforce that the CS2 is Pedersen commitment scheme, since we're at Ethereum's EVM decider
 68    CS2: CommitmentScheme<C2, ProverParams = PedersenParams<C2>>,
 69    S: SNARK<C1::ScalarField>,
 70    FS: FoldingScheme<C1, C2, FC>,
 71    <C1 as CurveGroup>::BaseField: PrimeField,
 72    <C2 as CurveGroup>::BaseField: PrimeField,
 73    <C1 as Group>::ScalarField: Absorb,
 74    <C2 as Group>::ScalarField: Absorb,
 75    C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
 76    for<'b> &'b GC1: GroupOpsBounds<'b, C1, GC1>,
 77    for<'b> &'b GC2: GroupOpsBounds<'b, C2, GC2>,
 78    // constrain FS into HyperNova, since this is a Decider specifically for HyperNova
 79    HyperNova<C1, GC1, C2, GC2, FC, CS1, CS2, MU, NU, false>: From<FS>,
 80    crate::folding::hypernova::ProverParams<C1, C2, CS1, CS2, false>:
 81        From<<FS as FoldingScheme<C1, C2, FC>>::ProverParam>,
 82    crate::folding::hypernova::VerifierParams<C1, C2, CS1, CS2, false>:
 83        From<<FS as FoldingScheme<C1, C2, FC>>::VerifierParam>,
 84{
 85    type PreprocessorParam = (FS::ProverParam, FS::VerifierParam);
 86    type ProverParam = (S::ProvingKey, CS1::ProverParams);
 87    type Proof = Proof<C1, CS1, S>;
 88    /// VerifierParam = (pp_hash, snark::vk, commitment_scheme::vk)
 89    type VerifierParam = (C1::ScalarField, S::VerifyingKey, CS1::VerifierParams);
 90    type PublicInput = Vec<C1::ScalarField>;
 91    type CommittedInstance = ();
 92
 93    fn preprocess(
 94        mut rng: impl RngCore + CryptoRng,
 95        prep_param: Self::PreprocessorParam,
 96        fs: FS,
 97    ) -> Result<(Self::ProverParam, Self::VerifierParam), Error> {
 98        let circuit =
 99            DeciderEthCircuit::<C1, GC1, C2, GC2, CS1, CS2>::from_hypernova::<FC, MU, NU>(
100                fs.into(),
101            )
102            .unwrap();
103
104        // get the Groth16 specific setup for the circuit
105        let (g16_pk, g16_vk) = S::circuit_specific_setup(circuit, &mut rng).unwrap();
106
107        // get the FoldingScheme prover & verifier params from HyperNova
108        #[allow(clippy::type_complexity)]
109        let hypernova_pp: <HyperNova<C1, GC1, C2, GC2, FC, CS1, CS2, MU, NU, false> as FoldingScheme<
110            C1,
111            C2,
112            FC,
113        >>::ProverParam = prep_param.0.into();
114        #[allow(clippy::type_complexity)]
115        let hypernova_vp: <HyperNova<C1, GC1, C2, GC2, FC, CS1, CS2, MU, NU, false> as FoldingScheme<
116            C1,
117            C2,
118            FC,
119        >>::VerifierParam = prep_param.1.into();
120        let pp_hash = hypernova_vp.pp_hash()?;
121
122        let pp = (g16_pk, hypernova_pp.cs_pp);
123        let vp = (pp_hash, g16_vk, hypernova_vp.cs_vp);
124        Ok((pp, vp))
125    }
126
127    fn prove(
128        mut rng: impl RngCore + CryptoRng,
129        pp: Self::ProverParam,
130        folding_scheme: FS,
131    ) -> Result<Self::Proof, Error> {
132        let (snark_pk, cs_pk): (S::ProvingKey, CS1::ProverParams) = pp;
133
134        let circuit = DeciderEthCircuit::<C1, GC1, C2, GC2, CS1, CS2>::from_hypernova::<FC, MU, NU>(
135            folding_scheme.into(),
136        )?;
137
138        let snark_proof = S::prove(&snark_pk, circuit.clone(), &mut rng)
139            .map_err(|e| Error::Other(e.to_string()))?;
140
141        // Notice that since the `circuit` has been constructed at the `from_hypernova` call, which
142        // in case of failure it would have returned an error there, the next two unwraps should
143        // never reach an error.
144        let rho_Fr = circuit.rho.ok_or(Error::Empty)?;
145        let W_i1 = circuit.W_i1.ok_or(Error::Empty)?;
146
147        // get the challenges that have been already computed when preparing the circuit inputs in
148        // the above `from_hypernova` call
149        let challenge_W = circuit
150            .kzg_challenge
151            .ok_or(Error::MissingValue("kzg_challenge".to_string()))?;
152
153        // generate KZG proofs
154        let U_cmW_proof = CS1::prove_with_challenge(
155            &cs_pk,
156            challenge_W,
157            &W_i1.w,
158            &C1::ScalarField::zero(),
159            None,
160        )?;
161
162        Ok(Self::Proof {
163            snark_proof,
164            kzg_proof: U_cmW_proof,
165            rho: rho_Fr,
166            U_i1: circuit.U_i1.ok_or(Error::Empty)?,
167            kzg_challenge: challenge_W,
168        })
169    }
170
171    fn verify(
172        vp: Self::VerifierParam,
173        i: C1::ScalarField,
174        z_0: Vec<C1::ScalarField>,
175        z_i: Vec<C1::ScalarField>,
176        // we don't use the instances at the verifier level, since we check them in-circuit
177        _running_instance: &Self::CommittedInstance,
178        _incoming_instance: &Self::CommittedInstance,
179        proof: &Self::Proof,
180    ) -> Result<bool, Error> {
181        if i <= C1::ScalarField::one() {
182            return Err(Error::NotEnoughSteps);
183        }
184
185        let (pp_hash, snark_vk, cs_vk): (C1::ScalarField, S::VerifyingKey, CS1::VerifierParams) =
186            vp;
187
188        // Note: the NIMFS proof is checked inside the DeciderEthCircuit, which ensures that the
189        // 'proof.U_i1' is correctly computed
190
191        let (cmC_x, cmC_y) = NonNativeAffineVar::inputize(proof.U_i1.C)?;
192
193        let public_input: Vec<C1::ScalarField> = [
194            vec![pp_hash, i],
195            z_0,
196            z_i,
197            // U_i+1:
198            cmC_x,
199            cmC_y,
200            vec![proof.U_i1.u],
201            proof.U_i1.x.clone(),
202            proof.U_i1.r_x.clone(),
203            proof.U_i1.v.clone(),
204            vec![proof.kzg_challenge, proof.kzg_proof.eval, proof.rho],
205        ]
206        .concat();
207
208        let snark_v = S::verify(&snark_vk, &public_input, &proof.snark_proof)
209            .map_err(|e| Error::Other(e.to_string()))?;
210        if !snark_v {
211            return Err(Error::SNARKVerificationFail);
212        }
213
214        // we're at the Ethereum EVM case, so the CS1 is KZG commitments
215        CS1::verify_with_challenge(&cs_vk, proof.kzg_challenge, &proof.U_i1.C, &proof.kzg_proof)?;
216
217        Ok(true)
218    }
219}
220
221#[cfg(test)]
222pub mod tests {
223    use ark_bn254::{constraints::GVar, Bn254, Fr, G1Projective as Projective};
224    use ark_groth16::Groth16;
225    use ark_grumpkin::{constraints::GVar as GVar2, Projective as Projective2};
226    use std::time::Instant;
227
228    use super::*;
229    use crate::commitment::{kzg::KZG, pedersen::Pedersen};
230    use crate::folding::hypernova::PreprocessorParam;
231    use crate::frontend::utils::CubicFCircuit;
232    use crate::transcript::poseidon::poseidon_canonical_config;
233
234    #[test]
235    fn test_decider() {
236        const MU: usize = 1;
237        const NU: usize = 1;
238        // use HyperNova as FoldingScheme
239        type HN = HyperNova<
240            Projective,
241            GVar,
242            Projective2,
243            GVar2,
244            CubicFCircuit<Fr>,
245            KZG<'static, Bn254>,
246            Pedersen<Projective2>,
247            MU,
248            NU,
249            false,
250        >;
251        type D = Decider<
252            Projective,
253            GVar,
254            Projective2,
255            GVar2,
256            CubicFCircuit<Fr>,
257            KZG<'static, Bn254>,
258            Pedersen<Projective2>,
259            Groth16<Bn254>, // here we define the Snark to use in the decider
260            HN,             // here we define the FoldingScheme to use
261            MU,
262            NU,
263        >;
264
265        let mut rng = ark_std::test_rng();
266        let poseidon_config = poseidon_canonical_config::<Fr>();
267
268        let F_circuit = CubicFCircuit::<Fr>::new(()).unwrap();
269        let z_0 = vec![Fr::from(3_u32)];
270
271        let prep_param = PreprocessorParam::new(poseidon_config, F_circuit);
272        let hypernova_params = HN::preprocess(&mut rng, &prep_param).unwrap();
273
274        let start = Instant::now();
275        let mut hypernova = HN::init(&hypernova_params, F_circuit, z_0.clone()).unwrap();
276        println!("Nova initialized, {:?}", start.elapsed());
277        let start = Instant::now();
278        hypernova
279            .prove_step(&mut rng, vec![], Some((vec![], vec![])))
280            .unwrap();
281        println!("prove_step, {:?}", start.elapsed());
282        hypernova
283            .prove_step(&mut rng, vec![], Some((vec![], vec![])))
284            .unwrap(); // do a 2nd step
285
286        let mut rng = rand::rngs::OsRng;
287
288        // prepare the Decider prover & verifier params
289        let (decider_pp, decider_vp) =
290            D::preprocess(&mut rng, hypernova_params, hypernova.clone()).unwrap();
291
292        // decider proof generation
293        let start = Instant::now();
294        let proof = D::prove(rng, decider_pp, hypernova.clone()).unwrap();
295        println!("Decider prove, {:?}", start.elapsed());
296
297        // decider proof verification
298        let start = Instant::now();
299        let verified = D::verify(
300            decider_vp,
301            hypernova.i,
302            hypernova.z_0,
303            hypernova.z_i,
304            &(),
305            &(),
306            &proof,
307        )
308        .unwrap();
309        assert!(verified);
310        println!("Decider verify, {:?}", start.elapsed());
311    }
312}