Verifier should check the commitments in committed instances

folding-schemes/src/folding/circuits/decider/mod.rs

@@ -104,6 +104,8 @@ pub trait DeciderEnabledNIFS<
 {
     type ProofDummyCfg;
     type Proof: Dummy<Self::ProofDummyCfg>;
+    type RandomnessDummyCfg;
+    type Randomness: Dummy<Self::RandomnessDummyCfg>;
 
     #[allow(clippy::too_many_arguments)]
     fn fold_gadget(
@@ -114,6 +116,7 @@ pub trait DeciderEnabledNIFS<
         U_vec: Vec<FpVar<CF1<C>>>,
         u: IU::Var,
         proof: Self::Proof,
+        randomness: Self::Randomness,
     ) -> Result<RU::Var, SynthesisError>;
 }
 

folding-schemes/src/folding/circuits/decider/off_chain.rs

@@ -25,6 +25,7 @@ use crate::{
                 CycleFoldCommittedInstance, CycleFoldCommittedInstanceVar, CycleFoldWitness,
             },
             decider::{EvalGadget, KZGChallengesGadget},
+            nonnative::affine::NonNativeAffineVar,
             CF1, CF2,
         },
         nova::{circuits::CommittedInstanceVar, decider_eth_circuit::WitnessVar},
@@ -69,6 +70,7 @@ pub struct GenericOffchainDeciderCircuit1<
 
     /// Helper for folding verification
     pub proof: D::Proof,
+    pub randomness: D::Randomness,
 
     /// CycleFold running instance
     pub cf_U_i: CycleFoldCommittedInstance<C2>,
@@ -94,16 +96,26 @@ impl<
         &R1CS<CF1<C2>>,
         PoseidonConfig<CF1<C1>>,
         D::ProofDummyCfg,
+        D::RandomnessDummyCfg,
         usize,
         usize,
     )> for GenericOffchainDeciderCircuit1<C1, C2, GC2, RU, IU, W, A, AVar, D>
 {
     fn dummy(
-        (arith, cf_arith, poseidon_config, proof_config, state_len, num_commitments): (
+        (
+            arith,
+            cf_arith,
+            poseidon_config,
+            proof_config,
+            randomness_config,
+            state_len,
+            num_commitments,
+        ): (
             A,
             &R1CS<CF1<C2>>,
             PoseidonConfig<CF1<C1>>,
             D::ProofDummyCfg,
+            D::RandomnessDummyCfg,
             usize,
             usize,
         ),
@@ -123,6 +135,7 @@ impl<
             U_i1: RU::dummy(&arith),
             W_i1: W::dummy(&arith),
             proof: D::Proof::dummy(proof_config),
+            randomness: D::Randomness::dummy(randomness_config),
             cf_U_i: CycleFoldCommittedInstance::dummy(cf_arith),
             kzg_challenges: vec![Zero::zero(); num_commitments],
             kzg_evaluations: vec![Zero::zero(); num_commitments],
@@ -144,7 +157,7 @@ impl<
     > ConstraintSynthesizer<CF1<C1>>
     for GenericOffchainDeciderCircuit1<C1, C2, GC2, RU, IU, W, A, AVar, D>
 where
-    RU::Var: AbsorbGadget<CF1<C1>>,
+    RU::Var: AbsorbGadget<CF1<C1>> + CommittedInstanceVarOps<C1, PointVar = NonNativeAffineVar<C1>>,
     CF1<C1>: Absorb,
 {
     fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C1>>) -> Result<(), SynthesisError> {
@@ -158,8 +171,12 @@ where
         let u_i = IU::Var::new_witness(cs.clone(), || Ok(self.u_i))?;
         let U_i = RU::Var::new_witness(cs.clone(), || Ok(self.U_i))?;
         // here (U_i1, W_i1) = NIFS.P( (U_i,W_i), (u_i,w_i))
-        let U_i1 = RU::Var::new_input(cs.clone(), || Ok(self.U_i1))?;
+        let U_i1_commitments = Vec::<NonNativeAffineVar<C1>>::new_input(cs.clone(), || {
+            Ok(self.U_i1.get_commitments())
+        })?;
+        let U_i1 = RU::Var::new_witness(cs.clone(), || Ok(self.U_i1))?;
         let W_i1 = W::Var::new_witness(cs.clone(), || Ok(self.W_i1))?;
+        U_i1.get_commitments().enforce_equal(&U_i1_commitments)?;
 
         let cf_U_i =
             CycleFoldCommittedInstanceVar::<C2, GC2>::new_input(cs.clone(), || Ok(self.cf_U_i))?;
@@ -194,6 +211,7 @@ where
             U_i_vec,
             u_i,
             self.proof,
+            self.randomness,
         )?
         .enforce_partial_equal(&U_i1)?;
 

folding-schemes/src/folding/circuits/decider/on_chain.rs

@@ -21,6 +21,7 @@ use crate::{
                 CycleFoldCommittedInstance, CycleFoldCommittedInstanceVar, CycleFoldWitness,
             },
             decider::{EvalGadget, KZGChallengesGadget},
+            nonnative::affine::NonNativeAffineVar,
             CF1, CF2,
         },
         traits::{CommittedInstanceOps, CommittedInstanceVarOps, Dummy, WitnessOps, WitnessVarOps},
@@ -97,6 +98,7 @@ pub struct GenericOnchainDeciderCircuit<
 
     /// Helper for folding verification
     pub proof: D::Proof,
+    pub randomness: D::Randomness,
 
     /// CycleFold running instance
     pub cf_U_i: CycleFoldCommittedInstance<C2>,
@@ -124,6 +126,7 @@ impl<
         PedersenParams<C2>,
         PoseidonConfig<CF1<C1>>,
         D::ProofDummyCfg,
+        D::RandomnessDummyCfg,
         usize,
         usize,
     )> for GenericOnchainDeciderCircuit<C1, C2, GC2, RU, IU, W, A, AVar, D>
@@ -135,6 +138,7 @@ impl<
             cf_pedersen_params,
             poseidon_config,
             proof_config,
+            randomness_config,
             state_len,
             num_commitments,
         ): (
@@ -143,6 +147,7 @@ impl<
             PedersenParams<C2>,
             PoseidonConfig<CF1<C1>>,
             D::ProofDummyCfg,
+            D::RandomnessDummyCfg,
             usize,
             usize,
         ),
@@ -163,6 +168,7 @@ impl<
             U_i1: RU::dummy(&arith),
             W_i1: W::dummy(&arith),
             proof: D::Proof::dummy(proof_config),
+            randomness: D::Randomness::dummy(randomness_config),
             cf_U_i: CycleFoldCommittedInstance::dummy(&cf_arith),
             cf_W_i: CycleFoldWitness::dummy(&cf_arith),
             kzg_challenges: vec![Zero::zero(); num_commitments],
@@ -186,7 +192,7 @@ impl<
     > ConstraintSynthesizer<CF1<C1>>
     for GenericOnchainDeciderCircuit<C1, C2, GC2, RU, IU, W, A, AVar, D>
 where
-    RU::Var: AbsorbGadget<CF1<C1>>,
+    RU::Var: AbsorbGadget<CF1<C1>> + CommittedInstanceVarOps<C1, PointVar = NonNativeAffineVar<C1>>,
     CF1<C1>: Absorb,
 {
     fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C1>>) -> Result<(), SynthesisError> {
@@ -200,8 +206,12 @@ where
         let u_i = IU::Var::new_witness(cs.clone(), || Ok(self.u_i))?;
         let U_i = RU::Var::new_witness(cs.clone(), || Ok(self.U_i))?;
         // here (U_i1, W_i1) = NIFS.P( (U_i,W_i), (u_i,w_i))
-        let U_i1 = RU::Var::new_input(cs.clone(), || Ok(self.U_i1))?;
+        let U_i1_commitments = Vec::<NonNativeAffineVar<C1>>::new_input(cs.clone(), || {
+            Ok(self.U_i1.get_commitments())
+        })?;
+        let U_i1 = RU::Var::new_witness(cs.clone(), || Ok(self.U_i1))?;
         let W_i1 = W::Var::new_witness(cs.clone(), || Ok(self.W_i1))?;
+        U_i1.get_commitments().enforce_equal(&U_i1_commitments)?;
 
         let cf_U_i =
             CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || Ok(self.cf_U_i))?;
@@ -291,6 +301,7 @@ where
             U_i_vec,
             u_i,
             self.proof,
+            self.randomness,
         )?
         .enforce_partial_equal(&U_i1)?;
 

folding-schemes/src/folding/circuits/nonnative/affine.rs

@@ -2,7 +2,9 @@ use ark_ec::{short_weierstrass::SWFlags, AffineRepr, CurveGroup};
 use ark_ff::{Field, PrimeField};
 use ark_r1cs_std::{
     alloc::{AllocVar, AllocationMode},
+    eq::EqGadget,
     fields::fp::FpVar,
+    prelude::Boolean,
     R1CSVar, ToConstraintFieldGadget,
 };
 use ark_relations::r1cs::{ConstraintSystemRef, Namespace, SynthesisError};
@@ -93,6 +95,53 @@ impl<C: CurveGroup> ToConstraintFieldGadget<C::ScalarField> for NonNativeAffineV
     }
 }
 
+impl<C: CurveGroup> EqGadget<C::ScalarField> for NonNativeAffineVar<C> {
+    fn is_eq(&self, other: &Self) -> Result<Boolean<C::ScalarField>, SynthesisError> {
+        let mut result = Boolean::TRUE;
+        if self.x.0.len() != other.x.0.len() {
+            return Err(SynthesisError::Unsatisfiable);
+        }
+        if self.y.0.len() != other.y.0.len() {
+            return Err(SynthesisError::Unsatisfiable);
+        }
+        for (l, r) in self
+            .x
+            .0
+            .iter()
+            .chain(&self.y.0)
+            .zip(other.x.0.iter().chain(&other.y.0))
+        {
+            if l.ub != r.ub {
+                return Err(SynthesisError::Unsatisfiable);
+            }
+            result = result.and(&l.v.is_eq(&r.v)?)?;
+        }
+        Ok(result)
+    }
+
+    fn enforce_equal(&self, other: &Self) -> Result<(), SynthesisError> {
+        if self.x.0.len() != other.x.0.len() {
+            return Err(SynthesisError::Unsatisfiable);
+        }
+        if self.y.0.len() != other.y.0.len() {
+            return Err(SynthesisError::Unsatisfiable);
+        }
+        for (l, r) in self
+            .x
+            .0
+            .iter()
+            .chain(&self.y.0)
+            .zip(other.x.0.iter().chain(&other.y.0))
+        {
+            if l.ub != r.ub {
+                return Err(SynthesisError::Unsatisfiable);
+            }
+            l.v.enforce_equal(&r.v)?;
+        }
+        Ok(())
+    }
+}
+
 /// The out-circuit counterpart of `NonNativeAffineVar::to_constraint_field`
 #[allow(clippy::type_complexity)]
 pub(crate) fn nonnative_affine_to_field_elements<C: CurveGroup>(

folding-schemes/src/folding/hypernova/decider_eth.rs

@@ -10,13 +10,13 @@ use ark_std::{One, Zero};
 use core::marker::PhantomData;
 
 pub use super::decider_eth_circuit::DeciderEthCircuit;
-use super::{lcccs::LCCCS, HyperNova};
+use super::HyperNova;
 use crate::commitment::{
     kzg::Proof as KZGProof, pedersen::Params as PedersenParams, CommitmentScheme,
 };
 use crate::folding::circuits::CF2;
 use crate::folding::nova::decider_eth::VerifierParam;
-use crate::folding::traits::{CommittedInstanceOps, Inputize, WitnessOps};
+use crate::folding::traits::{Inputize, WitnessOps};
 use crate::frontend::FCircuit;
 use crate::Error;
 use crate::{Decider as DeciderTrait, FoldingScheme};
@@ -30,7 +30,8 @@ where
 {
     snark_proof: S::Proof,
     kzg_proof: CS1::Proof,
-    U_final: LCCCS<C1>,
+    // rho used at the last fold, U_{i+1}=NIMFS.V(rho, U_i, u_i), it is checked in-circuit
+    rho: C1::ScalarField,
     // the KZG challenge is provided by the prover, but in-circuit it is checked to match
     // the in-circuit computed computed one.
     kzg_challenge: C1::ScalarField,
@@ -86,7 +87,7 @@ where
     type Proof = Proof<C1, CS1, S>;
     type VerifierParam = VerifierParam<C1, CS1::VerifierParams, S::VerifyingKey>;
     type PublicInput = Vec<C1::ScalarField>;
-    type CommittedInstance = ();
+    type CommittedInstance = Vec<C1>;
 
     fn preprocess(
         mut rng: impl RngCore + CryptoRng,
@@ -133,7 +134,7 @@ where
         let circuit =
             DeciderEthCircuit::<C1, C2, GC2>::try_from(HyperNova::from(folding_scheme)).unwrap();
 
-        let U_final = circuit.U_i1.clone();
+        let rho = circuit.randomness;
 
         // get the challenges that have been already computed when preparing the circuit inputs in
         // the above `try_from` call
@@ -155,7 +156,7 @@ where
 
         Ok(Self::Proof {
             snark_proof,
-            U_final,
+            rho,
             kzg_proof: (kzg_proofs.len() == 1)
                 .then(|| kzg_proofs[0].clone())
                 .ok_or(Error::NotExpectedLength(kzg_proofs.len(), 1))?,
@@ -171,8 +172,8 @@ where
         z_0: Vec<C1::ScalarField>,
         z_i: Vec<C1::ScalarField>,
         // we don't use the instances at the verifier level, since we check them in-circuit
-        _running_instance: &Self::CommittedInstance,
-        _incoming_instance: &Self::CommittedInstance,
+        running_commitments: &Self::CommittedInstance,
+        incoming_commitments: &Self::CommittedInstance,
         proof: &Self::Proof,
     ) -> Result<bool, Error> {
         if i <= C1::ScalarField::one() {
@@ -185,16 +186,18 @@ where
             cs_vp,
         } = vp;
 
-        let U = proof.U_final.clone();
+        let U_C = running_commitments[0];
+        let u_C = incoming_commitments[0];
+        let C = U_C + u_C.mul(proof.rho);
 
         // Note: the NIMFS proof is checked inside the DeciderEthCircuit, which ensures that the
         // 'proof.U_i1' is correctly computed
         let public_input: Vec<C1::ScalarField> = [
-            vec![pp_hash, i],
-            z_0,
-            z_i,
-            U.inputize(),
-            vec![proof.kzg_challenge, proof.kzg_proof.eval],
+            &[pp_hash, i][..],
+            &z_0,
+            &z_i,
+            &C.inputize(),
+            &[proof.kzg_challenge, proof.kzg_proof.eval, proof.rho],
         ]
         .concat();
 
@@ -204,18 +207,8 @@ where
             return Err(Error::SNARKVerificationFail);
         }
 
-        let commitments = U.get_commitments();
-        if commitments.len() != 1 {
-            return Err(Error::NotExpectedLength(commitments.len(), 1));
-        }
-
         // we're at the Ethereum EVM case, so the CS1 is KZG commitments
-        CS1::verify_with_challenge(
-            &cs_vp,
-            proof.kzg_challenge,
-            &commitments[0],
-            &proof.kzg_proof,
-        )?;
+        CS1::verify_with_challenge(&cs_vp, proof.kzg_challenge, &C, &proof.kzg_proof)?;
 
         Ok(true)
     }
@@ -231,9 +224,11 @@ pub mod tests {
     use super::*;
     use crate::commitment::{kzg::KZG, pedersen::Pedersen};
     use crate::folding::hypernova::cccs::CCCS;
+    use crate::folding::hypernova::lcccs::LCCCS;
     use crate::folding::hypernova::{
         PreprocessorParam, ProverParams, VerifierParams as HyperNovaVerifierParams,
     };
+    use crate::folding::traits::CommittedInstanceOps;
     use crate::frontend::utils::CubicFCircuit;
     use crate::transcript::poseidon::poseidon_canonical_config;
 
@@ -298,8 +293,8 @@ pub mod tests {
             hypernova.i,
             hypernova.z_0,
             hypernova.z_i,
-            &(),
-            &(),
+            &hypernova.U_i.get_commitments(),
+            &hypernova.u_i.get_commitments(),
             &proof,
         )
         .unwrap();
@@ -415,8 +410,8 @@ pub mod tests {
             hypernova.i,
             hypernova.z_0.clone(),
             hypernova.z_i.clone(),
-            &(),
-            &(),
+            &hypernova.U_i.get_commitments(),
+            &hypernova.u_i.get_commitments(),
             &proof,
         )
         .unwrap();
@@ -482,8 +477,8 @@ pub mod tests {
             i_deserialized,
             z_0_deserialized.clone(),
             z_i_deserialized.clone(),
-            &(),
-            &(),
+            &hypernova.U_i.get_commitments(),
+            &hypernova.u_i.get_commitments(),
             &proof_deserialized,
         )
         .unwrap();