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::CryptographicSpongeVar,
  5    poseidon::{constraints::PoseidonSpongeVar, PoseidonSponge},
  6    Absorb, CryptographicSponge,
  7};
  8use ark_ec::CurveGroup;
  9use ark_ff::PrimeField;
 10use ark_r1cs_std::{
 11    alloc::{AllocVar, AllocationMode},
 12    boolean::Boolean,
 13    eq::EqGadget,
 14    fields::fp::FpVar,
 15    prelude::CurveVar,
 16    ToConstraintFieldGadget,
 17};
 18use ark_relations::r1cs::{Namespace, SynthesisError};
 19use ark_std::{borrow::Borrow, log2, marker::PhantomData};
 20
 21use super::{
 22    circuits::{CCCSVar, LCCCSVar, NIMFSGadget, ProofVar as NIMFSProofVar},
 23    nimfs::{NIMFSProof, NIMFS},
 24    HyperNova, Witness, CCCS, LCCCS,
 25};
 26use crate::folding::circuits::{decider::on_chain::GenericOnchainDeciderCircuit, CF1, CF2};
 27use crate::folding::traits::{WitnessOps, WitnessVarOps};
 28use crate::frontend::FCircuit;
 29use crate::utils::gadgets::{eval_mle, MatrixGadget};
 30use crate::Error;
 31use crate::{
 32    arith::{
 33        ccs::{circuits::CCSMatricesVar, CCS},
 34        ArithGadget,
 35    },
 36    folding::circuits::decider::{EvalGadget, KZGChallengesGadget},
 37};
 38use crate::{
 39    commitment::{pedersen::Params as PedersenParams, CommitmentScheme},
 40    folding::circuits::decider::DeciderEnabledNIFS,
 41};
 42
 43impl<C: CurveGroup> ArithGadget<WitnessVar<CF1<C>>, LCCCSVar<C>> for CCSMatricesVar<CF1<C>> {
 44    type Evaluation = Vec<FpVar<CF1<C>>>;
 45
 46    fn eval_relation(
 47        &self,
 48        w: &WitnessVar<CF1<C>>,
 49        u: &LCCCSVar<C>,
 50    ) -> Result<Self::Evaluation, SynthesisError> {
 51        let z = [&[u.u.clone()][..], &u.x, &w.w].concat();
 52
 53        self.M
 54            .iter()
 55            .map(|M_j| {
 56                let s = log2(M_j.n_rows) as usize;
 57                let Mz = M_j.mul_vector(&z)?;
 58                Ok(eval_mle(s, Mz, u.r_x.clone()))
 59            })
 60            .collect()
 61    }
 62
 63    fn enforce_evaluation(
 64        _w: &WitnessVar<CF1<C>>,
 65        u: &LCCCSVar<C>,
 66        v: Self::Evaluation,
 67    ) -> Result<(), SynthesisError> {
 68        v.enforce_equal(&u.v)
 69    }
 70}
 71
 72/// In-circuit representation of the Witness associated to the CommittedInstance.
 73#[derive(Debug, Clone)]
 74pub struct WitnessVar<F: PrimeField> {
 75    pub w: Vec<FpVar<F>>,
 76    pub r_w: FpVar<F>,
 77}
 78
 79impl<F: PrimeField> AllocVar<Witness<F>, F> for WitnessVar<F> {
 80    fn new_variable<T: Borrow<Witness<F>>>(
 81        cs: impl Into<Namespace<F>>,
 82        f: impl FnOnce() -> Result<T, SynthesisError>,
 83        mode: AllocationMode,
 84    ) -> Result<Self, SynthesisError> {
 85        f().and_then(|val| {
 86            let cs = cs.into();
 87
 88            let w: Vec<FpVar<F>> =
 89                Vec::new_variable(cs.clone(), || Ok(val.borrow().w.clone()), mode)?;
 90            let r_w = FpVar::<F>::new_variable(cs.clone(), || Ok(val.borrow().r_w), mode)?;
 91
 92            Ok(Self { w, r_w })
 93        })
 94    }
 95}
 96
 97impl<F: PrimeField> WitnessVarOps<F> for WitnessVar<F> {
 98    fn get_openings(&self) -> Vec<(&[FpVar<F>], FpVar<F>)> {
 99        vec![(&self.w, self.r_w.clone())]
100    }
101}
102
103pub type DeciderEthCircuit<C1, C2, GC2> = GenericOnchainDeciderCircuit<
104    C1,
105    C2,
106    GC2,
107    LCCCS<C1>,
108    CCCS<C1>,
109    Witness<CF1<C1>>,
110    CCS<CF1<C1>>,
111    CCSMatricesVar<CF1<C1>>,
112    DeciderHyperNovaGadget,
113>;
114
115impl<
116        C1: CurveGroup,
117        GC1: CurveVar<C1, CF2<C1>> + ToConstraintFieldGadget<CF2<C1>>,
118        C2: CurveGroup,
119        GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
120        FC: FCircuit<C1::ScalarField>,
121        CS1: CommitmentScheme<C1, H>,
122        // enforce that the CS2 is Pedersen commitment scheme, since we're at Ethereum's EVM decider
123        CS2: CommitmentScheme<C2, H, ProverParams = PedersenParams<C2>>,
124        const MU: usize,
125        const NU: usize,
126        const H: bool,
127    > TryFrom<HyperNova<C1, GC1, C2, GC2, FC, CS1, CS2, MU, NU, H>>
128    for DeciderEthCircuit<C1, C2, GC2>
129where
130    CF1<C1>: Absorb,
131{
132    type Error = Error;
133
134    fn try_from(hn: HyperNova<C1, GC1, C2, GC2, FC, CS1, CS2, MU, NU, H>) -> Result<Self, Error> {
135        // compute the U_{i+1}, W_{i+1}, by folding the last running & incoming instances
136        let mut transcript = PoseidonSponge::<C1::ScalarField>::new(&hn.poseidon_config);
137        transcript.absorb(&hn.pp_hash);
138        let (nimfs_proof, U_i1, W_i1, rho) = NIMFS::<C1, PoseidonSponge<C1::ScalarField>>::prove(
139            &mut transcript,
140            &hn.ccs,
141            &[hn.U_i.clone()],
142            &[hn.u_i.clone()],
143            &[hn.W_i.clone()],
144            &[hn.w_i.clone()],
145        )?;
146
147        // compute the KZG challenges used as inputs in the circuit
148        let kzg_challenges = KZGChallengesGadget::get_challenges_native(&mut transcript, &U_i1);
149
150        // get KZG evals
151        let kzg_evaluations = W_i1
152            .get_openings()
153            .iter()
154            .zip(&kzg_challenges)
155            .map(|((v, _), &c)| EvalGadget::evaluate_native(v, c))
156            .collect::<Result<Vec<_>, _>>()?;
157
158        Ok(Self {
159            _gc2: PhantomData,
160            _avar: PhantomData,
161            arith: hn.ccs,
162            cf_arith: hn.cf_r1cs,
163            cf_pedersen_params: hn.cf_cs_pp,
164            poseidon_config: hn.poseidon_config,
165            pp_hash: hn.pp_hash,
166            i: hn.i,
167            z_0: hn.z_0,
168            z_i: hn.z_i,
169            U_i: hn.U_i,
170            W_i: hn.W_i,
171            u_i: hn.u_i,
172            w_i: hn.w_i,
173            U_i1,
174            W_i1,
175            proof: nimfs_proof,
176            randomness: rho,
177            cf_U_i: hn.cf_U_i,
178            cf_W_i: hn.cf_W_i,
179            kzg_challenges,
180            kzg_evaluations,
181        })
182    }
183}
184
185pub struct DeciderHyperNovaGadget;
186
187impl<C: CurveGroup> DeciderEnabledNIFS<C, LCCCS<C>, CCCS<C>, Witness<C::ScalarField>, CCS<CF1<C>>>
188    for DeciderHyperNovaGadget
189where
190    CF1<C>: Absorb,
191{
192    type ProofDummyCfg = (usize, usize, usize, usize);
193    type Proof = NIMFSProof<C>;
194    type Randomness = CF1<C>;
195    type RandomnessDummyCfg = ();
196
197    fn fold_field_elements_gadget(
198        arith: &CCS<CF1<C>>,
199        transcript: &mut PoseidonSpongeVar<CF1<C>>,
200        pp_hash: FpVar<CF1<C>>,
201        U: LCCCSVar<C>,
202        _U_vec: Vec<FpVar<CF1<C>>>,
203        u: CCCSVar<C>,
204        proof: Self::Proof,
205        randomness: Self::Randomness,
206    ) -> Result<LCCCSVar<C>, SynthesisError> {
207        let cs = transcript.cs();
208        transcript.absorb(&pp_hash)?;
209        let nimfs_proof = NIMFSProofVar::<C>::new_witness(cs.clone(), || Ok(proof))?;
210        let rho = FpVar::<CF1<C>>::new_input(cs.clone(), || Ok(randomness))?;
211        let (computed_U_i1, rho_bits) = NIMFSGadget::<C>::verify(
212            cs.clone(),
213            arith,
214            transcript,
215            &[U],
216            &[u],
217            nimfs_proof,
218            Boolean::TRUE, // enabled
219        )?;
220        Boolean::le_bits_to_fp_var(&rho_bits)?.enforce_equal(&rho)?;
221        Ok(computed_U_i1)
222    }
223
224    fn fold_group_elements_native(
225        U_commitments: &[C],
226        u_commitments: &[C],
227        _: Option<Self::Proof>,
228        r: Self::Randomness,
229    ) -> Result<Vec<C>, Error> {
230        let U_C = U_commitments[0];
231        let u_C = u_commitments[0];
232        let C = U_C + u_C.mul(r);
233        Ok(vec![C])
234    }
235}
236
237#[cfg(test)]
238pub mod tests {
239    use ark_bn254::{constraints::GVar, Fr, G1Projective as Projective};
240    use ark_grumpkin::{constraints::GVar as GVar2, Projective as Projective2};
241    use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystem};
242    use ark_std::{test_rng, UniformRand};
243
244    use super::*;
245    use crate::arith::r1cs::R1CS;
246    use crate::commitment::pedersen::Pedersen;
247    use crate::folding::nova::PreprocessorParam;
248    use crate::frontend::utils::CubicFCircuit;
249    use crate::transcript::poseidon::poseidon_canonical_config;
250    use crate::FoldingScheme;
251
252    #[test]
253    fn test_lcccs_checker_gadget() {
254        let mut rng = test_rng();
255        let n_rows = 2_u32.pow(5) as usize;
256        let n_cols = 2_u32.pow(5) as usize;
257        let r1cs = R1CS::<Fr>::rand(&mut rng, n_rows, n_cols);
258        let ccs = CCS::from(r1cs);
259        let z: Vec<Fr> = (0..n_cols).map(|_| Fr::rand(&mut rng)).collect();
260
261        let (pedersen_params, _) =
262            Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
263
264        let (lcccs, w) = ccs
265            .to_lcccs::<_, Projective, Pedersen<Projective>, false>(&mut rng, &pedersen_params, &z)
266            .unwrap();
267
268        let cs = ConstraintSystem::<Fr>::new_ref();
269
270        // CCS's (sparse) matrices are constants in the circuit
271        let ccs_mat = CCSMatricesVar::<Fr>::new_constant(cs.clone(), ccs.clone()).unwrap();
272        let w_var = WitnessVar::new_witness(cs.clone(), || Ok(w)).unwrap();
273        let lcccs_var = LCCCSVar::new_input(cs.clone(), || Ok(lcccs)).unwrap();
274
275        ccs_mat.enforce_relation(&w_var, &lcccs_var).unwrap();
276
277        assert!(cs.is_satisfied().unwrap());
278    }
279
280    #[test]
281    fn test_decider_circuit() {
282        let mut rng = ark_std::test_rng();
283        let poseidon_config = poseidon_canonical_config::<Fr>();
284
285        let F_circuit = CubicFCircuit::<Fr>::new(()).unwrap();
286        let z_0 = vec![Fr::from(3_u32)];
287
288        const MU: usize = 1;
289        const NU: usize = 1;
290
291        type HN = HyperNova<
292            Projective,
293            GVar,
294            Projective2,
295            GVar2,
296            CubicFCircuit<Fr>,
297            Pedersen<Projective>,
298            Pedersen<Projective2>,
299            MU,
300            NU,
301            false,
302        >;
303        let prep_param = PreprocessorParam::<
304            Projective,
305            Projective2,
306            CubicFCircuit<Fr>,
307            Pedersen<Projective>,
308            Pedersen<Projective2>,
309            false,
310        >::new(poseidon_config, F_circuit);
311        let hn_params = HN::preprocess(&mut rng, &prep_param).unwrap();
312
313        // generate a Nova instance and do a step of it
314        let mut hypernova = HN::init(&hn_params, F_circuit, z_0.clone()).unwrap();
315        hypernova.prove_step(&mut rng, vec![], None).unwrap();
316
317        let ivc_proof = hypernova.ivc_proof();
318        HN::verify(hn_params.1, ivc_proof).unwrap();
319
320        // load the DeciderEthCircuit from the generated Nova instance
321        let decider_circuit =
322            DeciderEthCircuit::<Projective, Projective2, GVar2>::try_from(hypernova).unwrap();
323
324        let cs = ConstraintSystem::<Fr>::new_ref();
325
326        // generate the constraints and check that are satisfied by the inputs
327        decider_circuit.generate_constraints(cs.clone()).unwrap();
328        assert!(cs.is_satisfied().unwrap());
329        dbg!(cs.num_constraints());
330    }
331}